mirror of
https://git.FreeBSD.org/ports.git
synced 2025-01-24 09:25:01 +00:00
0ece797080
PR: ports/131631 Submitted by: Andrew Bernard <andrewb@cs.cmu.edu> (maintainer)
12 lines
419 B
Plaintext
12 lines
419 B
Plaintext
--- doc/guide/Makefile.orig 2009-02-08 13:47:36.000000000 -0500
|
|
+++ doc/guide/Makefile 2009-02-08 13:23:38.000000000 -0500
|
|
@@ -39,7 +39,7 @@
|
|
twelf_toc.html : twelf.texi;
|
|
@echo "---------- Creating HTML: twelf_*.html"
|
|
$(texi2html) -menu -number -split_chapter twelf.texi;
|
|
- $(texi2html) -check *.html;
|
|
+# $(texi2html) -check *.html;
|
|
|
|
twelf.pdf : twelf.texi;
|
|
@echo "---------- Creating unindexed PDF: twelf.pdf"
|