diff options
| author | David Aspinall | 2004-02-08 12:39:06 +0000 |
|---|---|---|
| committer | David Aspinall | 2004-02-08 12:39:06 +0000 |
| commit | 68a98c42981c265eaafe8ef86f5533177adf8900 (patch) | |
| tree | 700466807e1baf66dadec507b8ce169439b04380 | |
| parent | c44780ae98d1fdb8fa3212209d883afa079de665 (diff) | |
Fix golive, add some .cvsignore to ignored files
| -rw-r--r-- | Makefile.devel | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/Makefile.devel b/Makefile.devel index 7a99af59..316f4055 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -130,7 +130,7 @@ RELEASEDIR = /tmp/proofgeneral-www/ # How to make the release "live". (Could be "true" to do nothing). # was: GOLIVE=true -GOLIVE="scp -pr $RELEASEDIR ssh.inf.ed.ac.uk:/group/project/proofgen/web/releases/" +GOLIVE=scp -pr $(RELEASEDIR) ssh.inf.ed.ac.uk:/group/projects/proofgen/web/releases/ CVSNAME = ProofGeneral @@ -162,7 +162,7 @@ NONDISTFILES=.cvsignore */.cvsignore Makefile.devel Makefile.xemacs doc/notes.tx # NB: these are *patterns* to exclude rather than files! # I would rather have files themselves to exclude, but # seems to be no way. -IGNOREDFILES=ProofGeneral*/TAGS ProofGeneral*/Makefile.devel ProofGeneral*/todo* ProofGeneral*/bugs ProofGeneral*/ChangeLog ProofGeneral*/doc/ProofGeneral.dvi ProofGeneral*/doc/ProofGeneral.ps.gz ProofGeneral*/doc/ProofGeneral.pdf ProofGeneral*/doc/PG-adapting.ps.gz ProofGeneral*/doc/PG-adapting.pdf ProofGeneral/*/todo etc/TESTS +IGNOREDFILES=ProofGeneral*/TAGS ProofGeneral*/Makefile.devel ProofGeneral*/todo* ProofGeneral*/bugs ProofGeneral*/ChangeLog ProofGeneral*/doc/ProofGeneral.dvi ProofGeneral*/doc/ProofGeneral.ps.gz ProofGeneral*/doc/ProofGeneral.pdf ProofGeneral*/doc/PG-adapting.ps.gz ProofGeneral*/doc/PG-adapting.pdf ProofGeneral/*/todo etc/TESTS *.cvsignore */*.cvsignore # Temporary directory to to build a distribution in DISTBUILDIR = /tmp/ProofGeneralRelease @@ -476,8 +476,9 @@ rpmrelease: rpm ## releaseclean: ## Clean up temporary directories after building dist/release. ## +DISTTEMPFILES releaseclean: - rm -rf $(DISTBUILDIR) $(RPMTOPDIR) + rm -rf $(DISTBUILDIR) $(RPMTOPDIR) $(DISTTEMPFILES) ############################################################ ## |
