diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-07-17 19:28:00 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-07-17 19:28:00 +0000 |
| commit | 7f1a49c8d55136a95f8cf9fecf0c946629845fa8 (patch) | |
| tree | b40903e4643b1b92519635d0d7d1d7f5690509eb /distrib/check-list | |
| parent | 5eb4ec77dbcc7f4fdbc342db67eeefd93af26d81 (diff) | |
camlp4 maintenant intégré à ocaml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5946 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'distrib/check-list')
| -rwxr-xr-x | distrib/check-list | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/distrib/check-list b/distrib/check-list index a2a7107b2..c0e547062 100755 --- a/distrib/check-list +++ b/distrib/check-list @@ -88,10 +88,3 @@ fi # echo "Wrong version of required Objective Caml in coq.spec ($ocamlversionspec)" # echo Aborting; exit 1 # fi - -camlp4version=`grep "You need Camlp4 .* or later" $CONFIGFILE | sed -e 's/.*Camlp4 \(.*\) or later.*/\1/'` -echo -n The configure file seems to require Camlp4 version $camlp4version ... -echo -n " is that OK? " -read a -if [ "$a" != 'y' -a "$a" != 'Y' ]; then echo Aborting; exit 1; fi -echo Check list completed |