Commit cd34bd75 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Restore check of Isabelle realizations.

parent 67627df0
......@@ -11,10 +11,9 @@ echo "Testing Isabelle realizations"
make GENERATED_PREFIX_ISABELLE="$TMPREAL/lib/isabelle" update-isabelle > /dev/null 2> /dev/null
LANG=C diff lib/isabelle $TMPREAL/lib/isabelle/realizations.* > $TMPREAL/diff-isabelle
if test -s "$TMPREAL/diff-isabelle"; then
echo "temporarily disabled"
#echo "Isabelle realizations FAILED, please regenerate and prove them"
#cat $TMPREAL/diff-isabelle
#res=1
echo "Isabelle realizations FAILED, please regenerate and prove them"
cat $TMPREAL/diff-isabelle
res=1
else
echo "Isabelle realizations OK"
fi
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment