Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-25 16:04:30 -0700 (Wed, 25 Sep 2002)
Revision: 3899
Log message:

      This commit switches the PRL mode output from using the mp12 font
      to using Unicode (UTF-8) encoding.
      
      I will post a separate message in the newsgroup about this switch.
      

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