blob: a63735cbe9177606d74f42ae542ed12abd155050 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
--- twelf-orig/doc/guide/Makefile 2002-09-24 13:59:23.000000000 +1000
+++ twelf/doc/guide/Makefile 2022-03-27 16:45:03.547456767 +1100
@@ -38,10 +38,12 @@
twelf_toc.html : twelf.texi;
@echo "---------- Creating HTML: twelf_*.html"
- $(texi2html) -menu -number -split_chapter twelf.texi;
- $(texi2html) -check *.html;
+ $(texi2html) -menu -number-sections -split_chapter twelf.texi;
+# $(texi2html) -check *.html;
twelf.pdf : twelf.texi;
+ @echo "---------- Removing old files: twelf.{aux,log}"
+ rm -f twelf.{aux,log};
@echo "---------- Creating unindexed PDF: twelf.pdf"
$(pdftex) twelf.texi;
@echo "---------- Creating index twelf.cps"
|
GitWeb
