aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/Makefile
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1999-08-19 14:32:52 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1999-08-19 14:32:52 +0000
commit14af5b36782fd84a55af0c665b09a38c8d69b195 (patch)
treeb4f8e057a4114a97889011c2cba28469e39fb861 /doc/Makefile
parentfd6f7ccd16bd8fb0041539b8c19c2f26c6338173 (diff)
Adjustments to remove .eps picture from front
Diffstat (limited to 'doc/Makefile')
-rw-r--r--doc/Makefile14
1 files changed, 12 insertions, 2 deletions
diff --git a/doc/Makefile b/doc/Makefile
index 9013b8f1..e89f3904 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -11,7 +11,7 @@
##
## Use:
## make info,dvi,pdf,html - build respective docs from texi source.
-## make doc - make all kinds of doc.
+## make doc - make default kinds of doc (dvi, info).
##
###########################################################################
@@ -66,8 +66,18 @@ default: doc
ProofGeneral.txt:
echo > ProofGeneral.txt
+# In fact, the flag seems not to work (why?),
+# so comment out the image line too.
+# NB! mustn't have another line with '@c image' in it.
ProofGeneral.eps:
- gunzip -c ProofGeneral.eps.gz > ProofGeneral.eps
+ if [ -f ProofGeneral.eps.gz ]; then gunzip -c ProofGeneral.eps.gz > ProofGeneral.eps; fi
+ if [ -f ProofGeneral.eps ]; then \
+ sed 's/@clear haveeps/@set haveeps/g' ProofGeneral.texi > pgt; \
+ sed 's/@c image{ProofGeneral}/@image{ProofGeneral}/g' pgt > ProofGeneral.texi; \
+ else \
+ sed 's/@set haveeps/@clear haveeps/g' ProofGeneral.texi > pgt; \
+ sed 's/@image{ProofGeneral}/@c image{ProofGeneral}/g' pgt > ProofGeneral.texi; \
+ fi
%.gz : %
gzip -f -9 $*