diff options
| author | Jim Fehrle | 2020-03-27 21:55:37 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-03-28 11:03:00 -0700 |
| commit | 2a803690d76724fd7c97288f208f3a1faf98eca1 (patch) | |
| tree | df8e01ca2073958c1d19222161717ea46189d128 /doc/tools/docgram/common.edit_mlg | |
| parent | 28081c1108a84050566d365bd665d05ee508ecce (diff) | |
Remove SearchAbout command, deprecated in 8.5
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 4 |
1 files changed, 0 insertions, 4 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: [ |