diff options
| author | Théo Zimmermann | 2020-03-29 17:32:27 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-29 17:32:27 +0200 |
| commit | 6455f44c7a6babb1f2490eaca216469e0c450a00 (patch) | |
| tree | 282a6883b83a2134574ab4a213d3cb73fd8dff03 /doc/tools | |
| parent | eb01bc0f7583ef958a32e88c05d82cb9ad791ac4 (diff) | |
| parent | 2a803690d76724fd7c97288f208f3a1faf98eca1 (diff) | |
Merge PR #11944: Remove SearchAbout command, deprecated in 8.5
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 4 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 4 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 4 |
3 files changed, 0 insertions, 12 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 88a5217652..60b845c4be 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1125,10 +1125,6 @@ query_command: [ | WITH "SearchRewrite" constr_pattern in_or_out_modules | REPLACE "Search" searchabout_query searchabout_queries "." | WITH "Search" searchabout_query searchabout_queries -| REPLACE "SearchAbout" searchabout_query searchabout_queries "." -| WITH "SearchAbout" searchabout_query searchabout_queries -| REPLACE "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "." -| WITH "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules ] vernac_toplevel: [ diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 241cf48cf1..272d17bb35 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1244,8 +1244,6 @@ query_command: [ | "SearchPattern" constr_pattern in_or_out_modules "." | "SearchRewrite" constr_pattern in_or_out_modules "." | "Search" searchabout_query searchabout_queries "." -| "SearchAbout" searchabout_query searchabout_queries "." -| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "." ] printable: [ @@ -2454,8 +2452,6 @@ as_or_and_ipat: [ eqn_ipat: [ | "eqn" ":" naming_intropattern -| "_eqn" ":" naming_intropattern -| "_eqn" | ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 38e7b781df..0c9d7a853b 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -918,8 +918,6 @@ command: [ | "SearchPattern" one_term OPT ne_in_or_out_modules | "SearchRewrite" one_term OPT ne_in_or_out_modules | "Search" searchabout_query OPT searchabout_queries -| "SearchAbout" searchabout_query OPT searchabout_queries -| "SearchAbout" "[" LIST1 searchabout_query "]" OPT ne_in_or_out_modules | "Time" command | "Redirect" string command | "Timeout" num command @@ -1441,8 +1439,6 @@ as_or_and_ipat: [ eqn_ipat: [ | "eqn" ":" naming_intropattern -| "_eqn" ":" naming_intropattern -| "_eqn" ] as_name: [ |