Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-16 23:36:23 -0700 (Wed, 16 Jun 2004)
Revision: 5914
Log message:

      Aleksey Nogin wrote:
      > % editor/ml/mpopt
      > Fatal error: exception Refine_error.MakeRefineError(TermType)(AddressType).RefineError("Shell_current.pid_of_string", _)
      
      Fixed.  The shell expected path of the form %s.%d.  The Shell_current
      session loader now catches the exception on garbage files, and ignores them.
      

Changes	Path
+8 -4	metaprl/support/shell/shell_current.ml