aboutsummaryrefslogtreecommitdiffhomepage
path: root/distrib/RH
diff options
context:
space:
mode:
authorGravatar courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-25 13:01:41 +0000
committerGravatar courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-25 13:01:41 +0000
commit8680aa0f0bfb5d258a05f4754ee1213ec0e5da9e (patch)
tree80ff5e5767d6f5586d2e339f88a626e9de2a6c9e /distrib/RH
parent4e3b6db89c4223c3563ed7fc7f92f78a95c99283 (diff)
modif pour RPM et Debian
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1715 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'distrib/RH')
-rw-r--r--distrib/RH/.cvsignore1
-rw-r--r--distrib/RH/coq.spec.tpl28
2 files changed, 3 insertions, 26 deletions
diff --git a/distrib/RH/.cvsignore b/distrib/RH/.cvsignore
index bfec41c5e..18eeb6844 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 44a14c7ea..6d8add631 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)