# HG changeset patch
# User lcp
# Date 754746349 -3600
# Node ID 921ad94fdddba8d57b7753c0ae84ee9854df0c28
# Parent  5729f67574737aa4f97a15e8d7677b07f82c47a6
now inspects FOLP_build_completed

diff -r 5729f6757473 -r 921ad94fdddb src/FOLP/ex/ROOT.ML
--- a/src/FOLP/ex/ROOT.ML	Wed Dec 01 12:41:25 1993 +0100
+++ b/src/FOLP/ex/ROOT.ML	Wed Dec 01 12:45:49 1993 +0100
@@ -8,6 +8,8 @@
 
 writeln"Root file for FOLP examples";
 
+FOLP_build_completed;	(*Cause examples to fail if FOLP did*)
+
 proof_timing := true;
 
 time_use     "ex/intro.ML";