HTML specification

diff --git a/spec/.gitignore b/spec/.gitignore
index 46180543a3338ce24e76f3dad20d15bd73baa92362a6cdd2159fc2d36f28da6e..bcf42efa8a96d97a2021355b59dc16675f5a439e266d793eca663651fe0b650b 100644 (file)
--- a/spec/.gitignore
+++ b/spec/.gitignore
@@ -1 +1,2 @@
-/index.info
+/spec.html/
+/spec.info

diff --git a/spec/mk-html b/spec/mk-html
new file mode 100755 (executable)
index 0000000..92a7108
--- /dev/null
+++ b/spec/mk-html
@@ -0,0 +1,10 @@
+#!/bin/sh -e
+
+makeinfo --html \
+    --set-customization-variable SECTION_NAME_IN_TITLE=1 \
+    --set-customization-variable TREE_TRANSFORMATIONS=complete_tree_nodes_menus \
+    --set-customization-variable ASCII_PUNCTUATION=1 \
+    --set-customization-variable NO_CSS=1 \
+    --set-customization-variable FORMAT_MENU=menu \
+    --set-customization-variable DATE_IN_HEADER=1 \
+    --output spec.html index.texi

diff --git a/spec/mk-info b/spec/mk-info
index 10752329df5b77ae36a6b6c10966d58109e669b707bcf9d3d6b0bd187827ac81..e762f1608ec2a707ca332406e8eedfc9686005799bbf4afbc33e7b6a477123f8 100755 (executable)
--- a/spec/mk-info
+++ b/spec/mk-info
@@ -4,4 +4,4 @@ makeinfo \
     --set-customization-variable SECTION_NAME_IN_TITLE=1 \
     --set-customization-variable TREE_TRANSFORMATIONS=complete_tree_nodes_menus \
     --set-customization-variable ASCII_PUNCTUATION=1 \
-    index.texi
+    --output spec.info index.texi