From 803ebd5ff5cc46f87b16103e2fee3243887e88d2 Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 12 Mar 2004 17:45:42 +0000
Subject: coq.spec n\'est plus parametre

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5470 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 distrib/RH/coq.spec     | 59 +++++++++++++++++++++++++++++++++++++++++++++++++
 distrib/RH/coq.spec.tpl | 55 ---------------------------------------------
 2 files changed, 59 insertions(+), 55 deletions(-)
 create mode 100644 distrib/RH/coq.spec
 delete mode 100644 distrib/RH/coq.spec.tpl

diff --git a/distrib/RH/coq.spec b/distrib/RH/coq.spec
new file mode 100644
index 0000000000..d52a3027c7
--- /dev/null
+++ b/distrib/RH/coq.spec
@@ -0,0 +1,59 @@
+# This file has been generated from RH/coq.spec.tpl
+# Do not edit
+Name: coq
+Version: 8.0
+Release: 1
+Summary: The Coq Proof Assistant
+Copyright: freely redistributable
+Group: Applications/Math
+Vendor: INRIA & LRI
+URL: http://coq.inria.fr
+Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.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.06
+
+
+%prep
+%setup
+
+%build
+./configure -bindir /usr/bin -libdir /usr/lib/coq -mandir /usr/man -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
+
+
+%clean
+make clean
+
+%install
+make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-coq
+# 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 -f ../../coq.list
+%defattr(-,root,root)
+
diff --git a/distrib/RH/coq.spec.tpl b/distrib/RH/coq.spec.tpl
deleted file mode 100644
index fa52d635d1..0000000000
--- a/distrib/RH/coq.spec.tpl
+++ /dev/null
@@ -1,55 +0,0 @@
-Name: coq
-Version: 8.0
-Release: 1
-Summary: The Coq Proof Assistant
-Copyright: freely redistributable
-Group: Applications/Math
-Vendor: INRIA & LRI
-URL: http://coq.inria.fr
-Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.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.06
-
-
-%prep
-%setup
-
-%build
-m4_include(do_build)
-
-%clean
-make clean
-
-%install
-make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-coq
-# 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
-%defattr(-,root,root)
-m4_include(coq.list)
-- 
cgit v1.2.3