From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001
From: Samuel Mimram <samuel.mimram@ens-lyon.org>
Date: Wed, 28 Jul 2004 21:54:47 +0000
Subject: Imported Upstream version 8.0pl1

---
 contrib/extraction/test/extract | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100755 contrib/extraction/test/extract

(limited to 'contrib/extraction/test/extract')

diff --git a/contrib/extraction/test/extract b/contrib/extraction/test/extract
new file mode 100755
index 00000000..83444be3
--- /dev/null
+++ b/contrib/extraction/test/extract
@@ -0,0 +1,12 @@
+#!/bin/sh
+rm -f /tmp/extr$$.v 
+vfile=`./ml2v $1`
+d=`dirname $vfile`
+n=`basename $vfile .v`
+if [ -e custom/$n ]; then cat custom/$n > /tmp/extr$$.v; fi  
+echo "Cd \"$d\". Extraction Library $n. " >> /tmp/extr$$.v
+../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v 
+out=$?
+rm -f /tmp/extr$$.v
+exit $out
+
-- 
cgit v1.2.3