Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-09 22:36:10 -0700 (Fri, 09 Jul 2004)
Revision: 6052
Log message:

      Added a "-batch" command-line option to MetaPRL that causes MetaPRL to be
      a bit quieter. "-batch" implies "-cli".
      

Changes  Path
+4 -4 metaprl/editor/ml/shell_mp.ml
+2 -1 metaprl/support/shell/shell.ml
+1 -1 metaprl/support/shell/shell_browser.ml
+4 -2 metaprl/support/shell/shell_state.ml
+2 -1 metaprl/support/shell/shell_state.mli
+1 -1 metaprl/util/status-all.sh