diff options
| author | Théo Zimmermann | 2020-01-08 22:12:27 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-01-08 22:12:27 +0100 |
| commit | c3721670ce1efe741e8edad78d0b7e1a1510c9c1 (patch) | |
| tree | 6b8eff8ca5f711bd6ca7d59d341056c149d76bcd /plugins/syntax/string_notation.mli | |
| parent | 4c06f2974f9c6780287156be9535415a09d9f38a (diff) | |
| parent | f6d4484dfcf538e92241ef27ecc76de8b8ee30ff (diff) | |
Merge PR #11375: Add note about default goal selector next to bullet docs
Reviewed-by: Zimmi48
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions