aboutsummaryrefslogtreecommitdiff
path: root/distrib/Makefile
diff options
context:
space:
mode:
authorherbelin2001-09-26 17:20:08 +0000
committerherbelin2001-09-26 17:20:08 +0000
commit6956430dc9be97a3b9318e615834d73b87bb5c99 (patch)
tree9317382a3b3defe0a50343d3c4cce2dbd85289e6 /distrib/Makefile
parent5e729651cac3cab2694ca5a010c8fa40722b85ad (diff)
MAJ contrib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2075 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'distrib/Makefile')
-rw-r--r--distrib/Makefile6
1 files changed, 6 insertions, 0 deletions
diff --git a/distrib/Makefile b/distrib/Makefile
index 77ac42e383..1ca6161872 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -3,6 +3,8 @@
sinclude config.distrib
LOCALARCH=`uname -m`
ARCH=`uname -m | sed -e 's/i.86/i386/'`
+#Pour MacOS X
+#ARCH=`uname -m | sed -e 's/Power Macintosh/MacOS-X/'`
SYSTEM=`uname -s`
ARCHBUILDROOT=$(DISTRIBDIR)/${ARCH}
@@ -204,6 +206,10 @@ contrib-tar-gz:
- rm -rf contrib-${VERSION}
@echo -n Exporting a fresh copy of the contribs...
cvs export -d contrib-${VERSION} -r $(DASHEDVERSION) contrib
+ @echo -n Removing the maintenance files ...
+ @rm -rf contrib-${VERSION}/*/*/bench.log
+ @rm -rf contrib-${VERSION}/Lyon/PROGRAMS
+ @find contrib-${VERSION} -name ".cvsignore" -exec rm {} \;
@echo done
- rm contrib-${VERSION}.tar.gz
@echo -n Building the tar.gz contrib package