renamed 'gc' switch to 'mm'; [backport:1.6] (#19187)

* renamed 'gc' switch to 'mm'; [backport:1.6]
* better docs
This commit is contained in:
Andreas Rumpf 2021-11-24 15:49:32 +01:00 • committed by GitHub
commit a0073d2d4c
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
11 changed files with 157 additions and 143 deletions

View file

@ -129,7 +129,7 @@ tut2.rst
tut3.rst
nimc.rst
niminst.rst
gc.rst
mm.rst
""".splitWhitespace().mapIt("doc" / it)
doc0 = """