diff options
Diffstat (limited to 'math/proofgeneral/files/patch-doc-Makefile.doc')
| -rw-r--r-- | math/proofgeneral/files/patch-doc-Makefile.doc | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/math/proofgeneral/files/patch-doc-Makefile.doc b/math/proofgeneral/files/patch-doc-Makefile.doc new file mode 100644 index 000000000000..9480f3be265c --- /dev/null +++ b/math/proofgeneral/files/patch-doc-Makefile.doc @@ -0,0 +1,17 @@ +--- doc/Makefile.doc.orig Sun Apr 18 09:39:58 2004 ++++ doc/Makefile.doc Fri Jul 22 22:10:05 2005 +@@ -152,10 +152,10 @@ + ## texi: update magic comments in texi from docstrings in code. + ## (developer use only!) + ## +-$(DOCNAME).texi: ../*/*.el +- $(MAKE) magic +-magic: +- $(EMACS) -l docstring-magic.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer ++#$(DOCNAME).texi: ../*/*.el ++# $(MAKE) magic ++#magic: ++# $(EMACS) -batch -l ../generic/texi-docstring-magic.el -l ../generic/proof-site.el -l ../generic/pg-user.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer + + + |