diff --git a/std.prelude b/std.prelude index 21a60aacb5..36063af764 100644 --- a/std.prelude +++ b/std.prelude @@ -187,7 +187,16 @@ in val _ = loadPath := tl (!loadPath) end; -val _ = ReadHMF.extend_path_with_includes {verbosity = 1, lpref = loadPath}; +val _ = let + val lpsize0 = length (!loadPath) +in + ReadHMF.extend_path_with_includes {verbosity = 0, lpref = loadPath}; + if length (!loadPath) <> lpsize0 then + print ("** Load path (see loadPath variable) now contains " ^ + Int.toString (length (!loadPath)) ^ + " entries\n** after consulting Holmakefiles\n\n") + else () +end; use (Path.concat(Globals.HOLDIR, "tools/check-intconfig.sml")); diff --git a/tools-poly/prelude.ML b/tools-poly/prelude.ML index 9a365c96c5..9d38535fb4 100644 --- a/tools-poly/prelude.ML +++ b/tools-poly/prelude.ML @@ -139,10 +139,16 @@ local end in val _ = HOL_Interactive.print_banner() + val lpsize0 = length (!loadPath) val () = ( hol_use ("help" ++ "src-sml") "Database" ; hol_use ("tools-poly" ++ "poly") "Help" ; ReadHMF.extend_path_with_includes {verbosity = 0, lpref = loadPath} + ; if length (!loadPath) <> lpsize0 then + print ("** Load path (see loadPath variable) now contains " ^ + Int.toString (length (!loadPath)) ^ + " entries\n** after consulting Holmakefiles\n\n") + else () ; List.app Meta.fakeload ["PP", "PolyML", "Posix"] ; Globals.interactive := true ; Parse.current_backend := Parse.interactive_ppbackend ()