*** empty log message ***

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

6 files changed, 27 insertions, 44 deletions

diff --git a/distrib/RH/.cvsignore b/distrib/RH/.cvsignore
index 18eeb6844..d7a4769a2 100644
--- a/distrib/RH/.cvsignore
+++ b/distrib/RH/.cvsignore
@@ -1,3 +1,5 @@
-build
-coq.list
-coq-7.0
+build src
+coq.list pcoq.list coqide.list
+pcoq.spec
+rpmmacros rpmrc
+coq-*
diff --git a/distrib/RH/coq.spec b/distrib/RH/coq.spec
index 89536cb83..c8945b4fa 100644
--- a/distrib/RH/coq.spec
+++ b/distrib/RH/coq.spec
@@ -26,15 +26,15 @@ Coq is a proof assistant which:
 %setup
 
 %build
-./configure -prefix /usr -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
-make coq                    # Use native coq to compile theories
+./configure -prefix /usr -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
+make coq       # Use native coq to compile theories
 
 
 %clean
 make clean
 
 %install
-make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ BASETEXDIR=$RPM_BUILD_ROOT/ install-coq
+make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-coq
 # To install only locally the binaries compiled with absolute paths
 
 %post
@@ -52,7 +52,8 @@ if [ -L /usr/local/lib/ocaml ]; then
   rm /usr/local/lib/ocaml
 fi
 
-# the spec file is moved to distrib/RH/src/SPECS but coq.list is in distrib/RH
+# the spec file is read from distrib/RH/src/SOURCES/coqX.Y
+# but coq.list is in distrib/RH/src
 %files -f ../../coq.list
 %defattr(-,root,root)
 
diff --git a/distrib/RH/coq_ext_for_pcoq.spec b/distrib/RH/coq_ext_for_pcoq.spec
index ebdea5ad0..f774372e6 100644
--- a/distrib/RH/coq_ext_for_pcoq.spec
+++ b/distrib/RH/coq_ext_for_pcoq.spec
@@ -6,7 +6,7 @@ Copyright: freely redistributable
 Group: Applications/Math
 Vendor: INRIA & LRI
 URL: http://coq.inria.fr
-Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq_ext_for_pcoq-8.0cdrom.tar.gz
+Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0cdrom.tar.gz
 Icon: petit-coq.gif
 Requires: coq = 8.0cdrom
 
@@ -15,21 +15,22 @@ The Coq Extension for Pcoq provides all facilities to interface Coq with
 Pcoq
 
 %prep
-%setup
+%setup -n coq-8.0cdrom
 
 %build
-./configure -prefix /usr -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
-make pcoq                   # Use native coq to compile theories
+./configure -prefix /usr -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
+make pcoq      # Use native coq to compile theories
 
 
 %clean
 make clean
 
 %install
-make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ BASETEXDIR=$RPM_BUILD_ROOT/ install-pcoq
+make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-pcoq
 # To install only locally the binaries compiled with absolute paths
 
-%files -f ../../coq-pcoq.list
-# the spec file is moved to distrib/RH/src/SPECS but coq.list is in distrib/RH
+# the spec file is read from distrib/RH/src/SOURCES/coqX.Y
+# but pcoq.list is in distrib/RH/src
+%files -f ../../pcoq.list
 %defattr(-,root,root)
 
diff --git a/distrib/RH/coqide.spec b/distrib/RH/coqide.spec
index b618fdafa..420589b26 100644
--- a/distrib/RH/coqide.spec
+++ b/distrib/RH/coqide.spec
@@ -18,38 +18,17 @@ Coq proof assistant
 %setup -n coq-8.0cdrom
 
 %build
-./configure -prefix /usr -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt -reals all   # Need ocamlc.opt and ocamlopt.opt
+./configure -prefix /usr -emacslib /usr/share/emacs/site-lisp -opt -reals all   # Need ocamlc.opt and ocamlopt.opt
 make coqide  # Use native coq to compile theories
 
 %clean
 make clean
 
 %install
-make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ BASETEXDIR=$RPM_BUILD_ROOT install-coqide
+make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-coqide
 # 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
+# the spec file is read from distrib/RH/src/SOURCES/coqX.Y
+# but coqide.list is in distrib/RH/src
+%files -f ../../coqide.list
 %defattr(-,root,root)
-/usr/bin/coqide.byte
-/usr/bin/coqide.opt
-/usr/bin/coqide
-/usr/lib/coq/ide/utf8.v
-/usr/lib/coq/ide/utf8.vo
-/usr/lib/coq/ide/coq.png
-/usr/lib/coq/ide/.coqide-gtk2rc
-/usr/lib/coq/ide/FAQ
diff --git a/distrib/RH/do_build b/distrib/RH/do_build
index 53abb8457..103d4a880 100644
--- a/distrib/RH/do_build
+++ b/distrib/RH/do_build
@@ -1,2 +1,2 @@
-./configure -prefix /usr -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
-make coq                    # Use native coq to compile theories
+./configure -prefix /usr -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
+make coq       # Use native coq to compile theories
diff --git a/distrib/RH/do_build_pcoq b/distrib/RH/do_build_pcoq
index 87ce91d55..0477d001b 100755
--- a/distrib/RH/do_build_pcoq
+++ b/distrib/RH/do_build_pcoq
@@ -1,2 +1,2 @@
-./configure -prefix /usr -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
-make pcoq                   # Use native coq to compile theories
+./configure -prefix /usr -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
+make pcoq      # Use native coq to compile theories