Auto merge of #2558 - RalfJung:tag-gc, r=saethlin

readme: tag-gc tweaks

r? `@saethlin`

Is this option truly needed often enough that it should be in the 'common' section? If not I vote for moving it to the 2nd section. Also `10,000` is a confusing way to write numbers in an international context (in many languages, `,` in a number plays the role of the point in English number notation, so using a space or underscore is less likely to lead to confusion).

0 files changed, 0 insertions, 0 deletions