diff options
| author | David Aspinall | 2002-07-19 09:18:28 +0000 |
|---|---|---|
| committer | David Aspinall | 2002-07-19 09:18:28 +0000 |
| commit | 30415e6d007f25c8bdedc907f387130cbec59187 (patch) | |
| tree | 34746012a65fc53fbf1fc948619a879daf297e1a | |
| parent | ab8b978e61b2e1412e34af38b429e29a08f0e61b (diff) | |
Ignore todo.defunct
| -rw-r--r-- | Makefile.devel | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.devel b/Makefile.devel index b8e660a1..c579cf42 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -156,7 +156,7 @@ NONDISTFILES=.cvsignore */.cvsignore html Makefile.devel Makefile.xemacs doc/not # 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*/Makefile.devel ProofGeneral*/todo 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 +IGNOREDFILES=ProofGeneral*/Makefile.devel ProofGeneral*/todo* 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 # Temporary directory to to build a distribution in DISTBUILDIR = /tmp/ProofGeneralRelease |