$HOME/.bashrc provides TZ for *all* processes, resulting in proper date for Build_Log.log_date in remote_build_history via ssh (see also fe8f8f88a1d7);

trim more thoroughly, e.g. trailing \0 seen on some system;

tuned;

build sha1 library;

proper CONFIG_SITE for msys;

clarified platform selection;

more robust Windows platform;

copy libgmp on Linux;

prefer raw Admin tool, without Isabelle settings environment;

clarified command-line;

no backup of generated stuff;

more precise environment (for Windows);

proper shell_path for msys inside cygwin;

support other bash executable (notably for msys on Windows);

proper options; simplified command-line; tuned;

build_polyml in Scala;

clarified File.move: target directory like File.copy;

more logging, to see better when files written;

proper cleanup;

uniform order for options and args;

more robust jedit_auto_resolve: avoid losing events deps_changed() / delay_load.invoke();

tuned comment;

proper option for "build", not "build_history" (cf. 5ca4ac099e94);

tuned;

simplified main proof;

misc tuning and modernization;

recovered Output.writeln for remote build_history (cf. ed8940d6295c), in order to have log files copied and removed;

more uniform path syntax, as in ML (see 5a7c919a4ada);