From 4ca67150e972899bc84e78c589833ba06a66aa21 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 27 Mar 2020 16:48:22 +0100
Subject: Update syntax of Import / Export in documentation.

---
 doc/tools/docgram/common.edit_mlg | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'doc/tools/docgram/common.edit_mlg')

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: [
-- 
cgit v1.2.3