diff -r 4a960c012383 -r 2e29baa12ae7 src/Modal/ex/ROOT.ML --- a/src/Modal/ex/ROOT.ML Tue Nov 21 12:43:09 1995 +0100 +++ b/src/Modal/ex/ROOT.ML Tue Nov 21 12:43:52 1995 +0100 @@ -25,6 +25,4 @@ time_use "ex/S4thms.ML"; time_use "ex/S43thms.ML"; -make_chart (); (*make HTML chart*) - maketest"END: Root file for Modal examples";