Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-21 03:46:52 -0700 (Mon, 21 Jun 2004)
Revision: 5977
Log message:

      Some of the code was attempting to add root to a file that already contained it,
      resulting in the wrong file name, which then was not added to the edit menu.
      I solved it by calling strip_root one extra time, but this whole sequence
      of strip root/add root/strip root seems wierd - hopefully Jason can simplify
      and fix it properly.
      

Changes	Path
+1 -2	metaprl/support/shell/session.ml