Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-12 15:10:22 -0800 (Tue, 12 Jan 1999)
Revision: 2567
Log message:

      Suffix for the Refiner module to use.
      Possible values: ds_verb, ds_simp, std_verb, std_simp
      
      The system looks for suffix to use:
       1) In .refiner file (if it's non-empty)
       2) In MP_REFINER environment variable (if set)
       3) Prints warning and uses "ds_verb"
      

Changes	Path
Properties	metaprl/refiner/refiner
+27 -0	metaprl/refiner/refiner/Makefile
Deleted	metaprl/refiner/refiner/refiner.ml