Reinstate (short!) message about changed loadPath when hol begins

(This fixes Moscow ML interactive behaviour to be the same also.)

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"));
 

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 ()