diff options
author | 1999-11-26 13:48:26 +0000 | |
---|---|---|
committer | 1999-11-26 13:48:26 +0000 | |
commit | 457ab8f22c504369f729c9969bb55b3cc878c3eb (patch) | |
tree | c60700a75a071d384696b250d11360590df4546e | |
parent | e01d5841b808cae3f43d857cc45dfa3832aded96 (diff) |
Added devel.links target to make a couple of handy links.
-rw-r--r-- | Makefile.devel | 14 |
1 files changed, 14 insertions, 0 deletions
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 + |