diff options
| author | Théo Zimmermann | 2020-03-27 16:48:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-13 15:18:18 +0200 |
| commit | 4ca67150e972899bc84e78c589833ba06a66aa21 (patch) | |
| tree | 46253957ab62b212e882362704b1c84d705236c9 /doc/tools/docgram/common.edit_mlg | |
| parent | ff99fb50b26ea4065daa8ae5b1c98ad5e6ba659a (diff) | |
Update syntax of Import / Export in documentation.
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index a01f57eb22..5034d9a3c9 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -511,6 +511,12 @@ strategy_flag: [ | OPTINREF ] +filtered_import: [ +| REPLACE global "(" LIST1 one_import_filter_name SEP "," ")" +| WITH global OPT [ "(" LIST1 one_import_filter_name SEP "," ")" ] +| DELETE global +] + functor_app_annot: [ | OPTINREF ] @@ -1582,6 +1588,7 @@ SPLICE: [ | searchabout_queries | locatable | scope_delimiter +| one_import_filter_name ] (* end SPLICE *) RENAME: [ |