diff options
Diffstat (limited to 'lang/twelf/files/patch-doc-guide-Makefile')
| -rw-r--r-- | lang/twelf/files/patch-doc-guide-Makefile | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/lang/twelf/files/patch-doc-guide-Makefile b/lang/twelf/files/patch-doc-guide-Makefile deleted file mode 100644 index 74b33913e7e4..000000000000 --- a/lang/twelf/files/patch-doc-guide-Makefile +++ /dev/null @@ -1,11 +0,0 @@ ---- 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" |