diff options
| author | barras | 2004-01-27 18:41:26 +0000 |
|---|---|---|
| committer | barras | 2004-01-27 18:41:26 +0000 |
| commit | e53708c1dd3be7b76d880e5d03fa3101eb44ac43 (patch) | |
| tree | ad010a8ffbaf4029d0911d56031998808f129a75 /distrib/RH | |
| parent | f1d2214ed54ab1afe1ffb8a3c5b36e37be48e847 (diff) | |
meilleure separation de compil et install de coq, coqide et coq-interface
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5256 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'distrib/RH')
| -rw-r--r-- | distrib/RH/coq.spec.tpl | 6 | ||||
| -rw-r--r-- | distrib/RH/coqide.spec | 5 | ||||
| -rw-r--r-- | distrib/RH/do_build | 2 |
3 files changed, 7 insertions, 6 deletions
diff --git a/distrib/RH/coq.spec.tpl b/distrib/RH/coq.spec.tpl index b466401d65..fa52d635d1 100644 --- a/distrib/RH/coq.spec.tpl +++ b/distrib/RH/coq.spec.tpl @@ -1,12 +1,12 @@ Name: coq -Version: 8.0beta +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.0beta/coq-8.0beta.tar.gz +Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.tar.gz Icon: petit-coq.gif %description @@ -32,7 +32,7 @@ m4_include(do_build) make clean %install -make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install +make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-coq # To install only locally the binaries compiled with absolute paths %post diff --git a/distrib/RH/coqide.spec b/distrib/RH/coqide.spec index 763b2cc6d6..515393690a 100644 --- a/distrib/RH/coqide.spec +++ b/distrib/RH/coqide.spec @@ -19,13 +19,13 @@ Coq proof assistant %build ./configure -bindir /usr/bin -libdir /usr/lib/coq -mandir /usr/man -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt -reals all # Need ocamlc.opt and ocamlopt.opt -make ide # Use native coq to compile theories +make coqide # Use native coq to compile theories %clean make clean %install -make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-ide +make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-coqide # To install only locally the binaries compiled with absolute paths %post @@ -48,6 +48,7 @@ fi /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 diff --git a/distrib/RH/do_build b/distrib/RH/do_build index db8fa10354..0b12ccba9e 100644 --- a/distrib/RH/do_build +++ b/distrib/RH/do_build @@ -1,2 +1,2 @@ ./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 world # Use native coq to compile theories +make coq # Use native coq to compile theories |