diff options
Diffstat (limited to 'test-suite/check')
| -rwxr-xr-x | test-suite/check | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/check b/test-suite/check index c5636a820a..06df1a12cd 100755 --- a/test-suite/check +++ b/test-suite/check @@ -232,6 +232,7 @@ test_misc () { # Non-standard features # Test xml compilation + nbtests=`expr $nbtests + 1` printf " xml..." COQ_XML_LIBRARY_ROOT=misc/xml $bincoqc -xml misc/berardi_test > /dev/null 2>&1 if [ ! -d misc/xml ]; then |