now declares FOLP_build_completed
authorlcp
Wed Dec 01 12:41:25 1993 +0100 (1993-12-01)
changeset 1765729f6757473
parent 175 c02750f7f604
child 177 921ad94fdddb
now declares FOLP_build_completed
src/FOLP/ROOT.ML
     1.1 --- a/src/FOLP/ROOT.ML	Tue Nov 30 15:31:07 1993 +0100
     1.2 +++ b/src/FOLP/ROOT.ML	Wed Dec 01 12:41:25 1993 +0100
     1.3 @@ -79,3 +79,5 @@
     1.4  
     1.5  use "../Pure/install_pp.ML";
     1.6  print_depth 8;
     1.7 +
     1.8 +val FOLP_build_completed = ();	(*indicate successful build*)