diff options
Diffstat (limited to 'Docs')
| -rwxr-xr-x | Docs/Support/test-make-manual | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/Docs/Support/test-make-manual b/Docs/Support/test-make-manual new file mode 100755 index 00000000000..52434bcea55 --- /dev/null +++ b/Docs/Support/test-make-manual @@ -0,0 +1,13 @@ +#!/bin/sh + +echo +echo "|---- Running makeinfo ----|" +makeinfo --no-split -I . manual.texi + +echo +echo "|---- Running texi2html ----|" +/usr/bin/perl ./Support/texi2html -iso -number manual.texi + +echo +echo "Please examine your modifications in \`manual.html'." +echo |