diff options
author | bors[bot] <26634292+bors[bot]@users.noreply.github.com> | 2020-11-02 17:34:41 +0000 |
---|---|---|
committer | GitHub <[email protected]> | 2020-11-02 17:34:41 +0000 |
commit | 2bd26e6afcdd7a75e1256987e5e3b460451dfff4 (patch) | |
tree | 97141ffe6090ad7b5092a4e57be22592bc6c3fcb /docs/dev/syntax.md | |
parent | eb4e84ff510b9e5ead529dba83fc1679a569c448 (diff) | |
parent | 58e3fd8e8e04a8436b17ca07bea5e791d1c01e65 (diff) |
Merge #6443
6443: Remove unnecessary clone r=jonas-schievink a=jonas-schievink
bors r+ :robot:
Co-authored-by: Jonas Schievink <[email protected]>
Diffstat (limited to 'docs/dev/syntax.md')
0 files changed, 0 insertions, 0 deletions