Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-09-19 12:51:58 -0700 (Wed, 19 Sep 2001)
Revision: 3386
Log message:

      Trying to make Java editor work with JDK 1.3.1. I fixed some of the problems,
      but it still does not work.
      

Changes	Path
+1 -1	metaprl/editor/java/Makefile
+4 -5	metaprl/editor/java/Nuprl.java
+1 -1	metaprl/editor/java/NuprlCommand.java
+2 -4	metaprl/editor/java/NuprlHost.java
+2 -4	metaprl/editor/java/NuprlLogin.java
+27 -20	metaprl/editor/java/NuprlManager.java
+2 -0	metaprl/editor/java/NuprlMenu.java
+4 -0	metaprl/editor/java/NuprlProof.java