From: Luca Padovani Date: Wed, 16 Jul 2003 08:45:34 +0000 (+0000) Subject: * updated the help file to reflect the new syntax (reload/remove) X-Git-Tag: LucaOK~77 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=7ddef45b3b2c42dd02bf86a1d426e3216f9ef882 * updated the help file to reflect the new syntax (reload/remove) --- diff --git a/helm/uwobo/uwobo_common.ml b/helm/uwobo/uwobo_common.ml index 84ba19967..b4a910f9d 100644 --- a/helm/uwobo/uwobo_common.ml +++ b/helm/uwobo/uwobo_common.ml @@ -86,12 +86,12 @@ let usage_string = key

- remove[?keys=key1,key2,...]
+ remove?keys=[key1,key2,...]
unload stylesheets specified by key1, key2, ... or all stylesheets if no key was given

- reload[?keys=key1,key2,...]
+ reload?keys=[key1,key2,...]
reload stylesheets specified by key1, key2, ... or all stylesheets if no key was given