Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-21 03:27:46 -0700 (Sat, 21 Sep 2002)
Revision: 3891
Log message:
Degree sign.
| Changes | Path |
| +1 -2 | metaprl/editor/fonts/charset.txt |
| +1 -1 | metaprl/editor/ml/mpconfig |
| +107 -107 | metaprl/theories/tactic/nuprl_font.ml |