summaryrefslogtreecommitdiff
path: root/src/HelpFile
diff options
context:
space:
mode:
authoraarne <unknown>2005-04-01 20:24:24 +0000
committeraarne <unknown>2005-04-01 20:24:24 +0000
commit3f91f61735ed8741d9601c8e2349336a7deb61a7 (patch)
tree3634ec9728fdf2559ca546b71e9f31e97fe88461 /src/HelpFile
parent75c08d7abfbfd533a33d772c650036178c887149 (diff)
mapStr ; appPredefined in err monad
Diffstat (limited to 'src/HelpFile')
-rw-r--r--src/HelpFile1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/HelpFile b/src/HelpFile
index 22e697da6..ead186001 100644
--- a/src/HelpFile
+++ b/src/HelpFile
@@ -38,6 +38,7 @@ i, import: i File
-res set the name used for resource (with -old option)
-path use the (colon-separated) search path to find modules
-optimize select an optimization to override file-defined flags
+ -conversion select parsing method (values strict|nondet)
examples:
i English.gf -- ordinary import of Concrete
i -retain german/ParadigmsGer.gf -- import of Resource to test