Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-21 03:30:34 -0700 (Sat, 21 Sep 2002)
Revision: 3892
Log message:

      Inmy previous commit I've accidentally included my Unicode changes.
      
      While they are probably the right thing, I am not sure if we are ready to switch
      to Unicode, so reverting for now.
      

Changes	Path
+1 -1	metaprl/editor/ml/mpconfig
+107 -107	metaprl/theories/tactic/nuprl_font.ml