From 457ab8f22c504369f729c9969bb55b3cc878c3eb Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Fri, 26 Nov 1999 13:48:26 +0000
Subject: Added devel.links target to make a couple of handy links.

---
 Makefile.devel | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/Makefile.devel b/Makefile.devel
index 2108538f..a6406d55 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -198,6 +198,9 @@ clean:
 	find . \( -name '*~' -o -name '#*#' -o -name '\.#.*' \) -print | xargs rm -f
 	(cd doc; $(MAKE) clean)
 	(cd images; $(MAKE) clean)
+	rm -f doc/ProofGeneralPortrait.eps.gz
+	rm -f html/ProofGeneral
+
 
 
 ############################################################
@@ -461,3 +464,14 @@ distinstall:
 	(cd $(DISTINSTALLDIR); \
 	 $(TAR) -xpzf $(DISTBUILDIR)/$(RELEASENAMETARGZ); \
 	 mv $(RELEASENAME) $(NAME))
+
+############################################################
+#
+# links:
+#   
+#   Make some handy links for developers.
+#
+links:
+	ln -sf ../html/ProofGeneralPortrait.eps.gz doc
+	ln -sf ../../ProofGeneral html
+
-- 
cgit v1.2.3