diff options
| author | Emilio Jesus Gallego Arias | 2019-06-06 17:52:51 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-06 17:52:51 +0200 |
| commit | c5798a8e041abf0b021c0820f7e6a5436729827e (patch) | |
| tree | f6f67101eb9da176bf5ea9984e8673bbc67b6969 /plugins/syntax/string_notation.ml | |
| parent | 281faca10d471be5fd2bca864ffd382d69f7a110 (diff) | |
| parent | df804ec5ddfacc6ceb88bae43405ebceeef67217 (diff) | |
Merge PR #10323: Remove old overlays
Reviewed-by: ejgallego
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions