aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorbarras2004-03-12 17:45:42 +0000
committerbarras2004-03-12 17:45:42 +0000
commit803ebd5ff5cc46f87b16103e2fee3243887e88d2 (patch)
tree1eb875a23c268d5e9c88166ca4db0f7376d0ac0d
parent5e436269003ba9e6db4d0e94dfe571b42e5d13fd (diff)
coq.spec n\'est plus parametre
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5470 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--distrib/RH/coq.spec (renamed from distrib/RH/coq.spec.tpl)10
1 files changed, 7 insertions, 3 deletions
diff --git a/distrib/RH/coq.spec.tpl b/distrib/RH/coq.spec
index fa52d635d1..d52a3027c7 100644
--- a/distrib/RH/coq.spec.tpl
+++ b/distrib/RH/coq.spec
@@ -1,3 +1,5 @@
+# This file has been generated from RH/coq.spec.tpl
+# Do not edit
Name: coq
Version: 8.0
Release: 1
@@ -26,7 +28,9 @@ Coq is a proof assistant which:
%setup
%build
-m4_include(do_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
@@ -50,6 +54,6 @@ if [ -L /usr/local/lib/ocaml ]; then
rm /usr/local/lib/ocaml
fi
-%files
+%files -f ../../coq.list
%defattr(-,root,root)
-m4_include(coq.list)
+