1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
Description: Update the documentation generation to suit Debian.
Since the source for the documentation is not packaged on Debian,
the special entrypoint for the documentation is disabled and
replaced with a message informing users of the location of the
pre-packaged documentation.
Forwarded: not-needed
Author: Filip Strömbäck <filip@fprg.se>
--- a/root/markdown/doc/main.bs
+++ b/root/markdown/doc/main.bs
@@ -180,27 +180,8 @@
// Convenience function to generate the Storm documentation.
Int generateStormDoc() {
- var root = core:lang:rootPkg;
- if (url = root.url) {
- var docRoot = url / ".." / "doc";
- Options options("Storm", "storm", docRoot, Url());
-
- var args = argv;
- Nat pos = options.applyOptions(args, 0);
- if (pos >= args.count) {
- print("Error: Expected an output path!");
- return 1;
- }
- options.output = parsePath(args[pos++]).makeAbsolute(cwdUrl);
-
- pos = options.applyOptions(args, pos);
- if (pos != args.count) {
- print("Error: Too many parameters!");
- return 1;
- }
-
- generate(options);
- return 0;
- }
- return 2;
+ print("On Debian systems, the HTML version is available");
+ print("in /usr/share/doc/storm-lang/html, if the package");
+ print("storm-lang-doc is installed.");
+ return 1;
}
|
