modif pour RPM et Debian

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1715 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 11 insertions, 108 deletions

diff --git a/distrib/Makefile b/distrib/Makefile
index 78149f7307..c03bb75be7 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -187,10 +187,14 @@ RH/coq.list: ${COQPACKAGE}.tar.gz Makefile config.distrib
 	cd RH ; tar xzf ../${COQPACKAGE}.tar.gz
 	cd RH/${COQPACKAGE} ; sh ../do_build
 	cd RH/${COQPACKAGE} ; make COQINSTALLPREFIX=${DISTRIBDIR}/RH/build install
-	cd RH/build ; find . '!' -type d > ../coq.list
+	echo "# This file has been generated" > RH/coq.list
+	echo "# Do not edit" >>RH/coq.list
+	cd RH/build ; find . '!' -type d | sed -e 's|^\./|/|g'>> ../coq.list
 
 coq.spec: RH/coq.list RH/coq.spec.tpl
-	cd RH ; m4 -P coq.spec.tpl > ../coq.spec
+	echo "# This file has been generated from RH/coq.spec.tpl" > coq.spec
+	echo "# Do not edit" >> coq.spec
+	cd RH ; m4 -P coq.spec.tpl >> ../coq.spec
 
 ##########
 contrib-tag:
diff --git a/distrib/RH/.cvsignore b/distrib/RH/.cvsignore
index bfec41c5e6..18eeb68449 100644
--- a/distrib/RH/.cvsignore
+++ b/distrib/RH/.cvsignore
@@ -1,2 +1,3 @@
 build
 coq.list
+coq-7.0
diff --git a/distrib/RH/coq.spec.tpl b/distrib/RH/coq.spec.tpl
index 44a14c7ea7..6d8add6318 100644
--- a/distrib/RH/coq.spec.tpl
+++ b/distrib/RH/coq.spec.tpl
@@ -26,7 +26,7 @@ Coq is a proof assistant which:
 %setup
 
 %build
-m4_include(coq.list)
+m4_include(do_build)
 
 %clean
 make clean
@@ -51,28 +51,4 @@ if [ -L /usr/local/lib/ocaml ]; then
 fi
 
 %files
-/usr/bin/coqc
-/usr/bin/coqtop
-/usr/bin/coqtop.byte
-/usr/bin/coqtop.opt
-/usr/bin/coq-tex
-/usr/bin/coqdep
-/usr/bin/gallina
-/usr/bin/coq_makefile
-/usr/bin/coq-interface
-/usr/bin/parser
-#/usr/bin/coq_searchisos.out
-/usr/bin/coqmktop
-#/usr/bin/coq2html
-#/usr/bin/coq2latex
-/usr/lib/coq
-#/usr/man/man1/coqc.1
-#/usr/man/man1/coqtop.1
-#/usr/man/man1/coqmktop.1
-/usr/man/man1/coqdep.1
-/usr/man/man1/gallina.1
-/usr/man/man1/coq-tex.1
-#/usr/man/man1/coq2latex.1
-#/usr/man/man1/coq2html.1
-/usr/share/emacs/site-lisp/coq.el
-/usr/share/emacs/site-lisp/coq.elc
+m4_include(coq.list)
diff --git a/distrib/coq.spec b/distrib/coq.spec
deleted file mode 100644
index 34954c6e42..0000000000
--- a/distrib/coq.spec
+++ /dev/null
@@ -1,79 +0,0 @@
-Name: coq
-Version: 7.0beta4
-Release: 1
-Summary: The Coq Proof Assistant
-Copyright: freely redistributable
-Group: Applications/Math
-Vendor: INRIA Rocquencourt
-URL: http://coq.inria.fr
-Source: ftp://ftp.inria.fr/INRIA/coq/V7.0/coq-7.0beta4.tar.gz
-Icon: petit-coq.gif
-
-%description
-Coq is a proof assistant which: 
-  - allows to handle calculus assertions, 
-  - check mechanically proofs of these assertions, 
-  - helps to find formal proofs, 
-  - extracts a certified program from the constructive proof
-    of its formal specification, 
-
-# Ocaml is required but it is better to install it not with rpm but by
-# hand in /usr/local
-# Requires: ocaml >= 3.01
-
-
-%prep
-%setup
-
-%build
-./configure -bindir /usr/bin -libdir /usr/lib/coq -mandir /usr/man -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt         # Need ocamlc.opt and ocamlopt.opt
-make world       # Use native coq to compile theories
-
-%clean
-make clean
-
-%install
-make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install
-# To install only locally the binaries compiled with absolute paths
-
-%post
-# This is a because the Coq Team usually build Coq with Ocaml in /usr/local
-# but ocaml is actually in /usr if coming from a rpm package
-# This works only if ocaml has been installed by rpm
-if [ ! -e /usr/local/lib/ocaml ]; then
-  ln -s /usr/lib/ocaml /usr/local/lib/ocaml || true
-fi
-
-%postun
-# This is because the Coq Team usually build Coq with Ocaml in /usr/local
-# but ocaml is actually in /usr if coming from a rpm package
-if [ -L /usr/local/lib/ocaml ]; then
-  rm /usr/local/lib/ocaml
-fi
-
-%files
-/usr/bin/coqc
-/usr/bin/coqtop
-/usr/bin/coqtop.byte
-/usr/bin/coqtop.opt
-/usr/bin/coq-tex
-/usr/bin/coqdep
-/usr/bin/gallina
-/usr/bin/coq_makefile
-/usr/bin/coq-interface
-/usr/bin/parser
-#/usr/bin/coq_searchisos.out
-/usr/bin/coqmktop
-#/usr/bin/coq2html
-#/usr/bin/coq2latex
-/usr/lib/coq
-#/usr/man/man1/coqc.1
-#/usr/man/man1/coqtop.1
-#/usr/man/man1/coqmktop.1
-/usr/man/man1/coqdep.1
-/usr/man/man1/gallina.1
-/usr/man/man1/coq-tex.1
-#/usr/man/man1/coq2latex.1
-#/usr/man/man1/coq2html.1
-/usr/share/emacs/site-lisp/coq.el
-/usr/share/emacs/site-lisp/coq.elc
diff --git a/distrib/debian/changelog b/distrib/debian/changelog
index 789b524e69..65d7fa05fb 100644
--- a/distrib/debian/changelog
+++ b/distrib/debian/changelog
@@ -1,8 +1,9 @@
-coq (7.0.0-1) unstable; urgency=low
+coq (7.0-1) unstable; urgency=low
   * New maintainer Judicaël Courant <Judicael.Courant@lri.fr>.
   * New upstream version.
   * Added Build-Depends (closes: Bug#70273).
   * Cleaned up dependencies.
+  * emacs mode installation now follows Emacs policy.
   * Made compilation non-interactive (closes: Bug#92461).