src/Pure/System/build.ML
2012-07-24 wenzelm 2012-07-24 added "browser_info_remote" (cf. usedir -P);
2012-07-24 wenzelm 2012-07-24 clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;
2012-07-24 wenzelm 2012-07-24 timing for whole session;
2012-07-24 wenzelm 2012-07-24 tuned options;
2012-07-24 wenzelm 2012-07-24 timing is command line options, not system option;
2012-07-24 wenzelm 2012-07-24 clarified document options;
2012-07-24 wenzelm 2012-07-24 pass build options to ML; some imitation of usedir Session.init;
2012-07-21 wenzelm 2012-07-21 save image for inner nodes only; misc tuning and simplification;
2012-07-21 wenzelm 2012-07-21 some actual build function on ML side; further imitation of "usedir" shell script;