diff options
| author | filliatr | 2001-04-19 15:07:41 +0000 |
|---|---|---|
| committer | filliatr | 2001-04-19 15:07:41 +0000 |
| commit | 8a009c8729dd6905dd7d47877b444fa38dd2e221 (patch) | |
| tree | 70f689960f99506af4f3d56796ea972e47193f21 /contrib/extraction/test/extract | |
| parent | fe45801c1fdfebeacaf5daa0569d89838b11774f (diff) | |
blindage False_rec
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1634 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/test/extract')
| -rwxr-xr-x | contrib/extraction/test/extract | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/test/extract b/contrib/extraction/test/extract index 1b0886a7e9..b5d6a6a787 100755 --- a/contrib/extraction/test/extract +++ b/contrib/extraction/test/extract @@ -3,6 +3,6 @@ rm -f /tmp/extr.v d=`dirname $1` n=`basename $1 .v` echo "Cd \"$d\". Extraction Module $n. " > /tmp/extr$$.v;\ -(../../../bin/coqtop.opt -batch -require $n -load-vernac-source /tmp/extr$$.v && rm -f /tmp/extr$$.v) || (rm -f /tmp/extr$$.v; exit 1) +(../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v && rm -f /tmp/extr$$.v) || (rm -f /tmp/extr$$.v; exit 1) |