diff options
| author | Emilio Jesus Gallego Arias | 2019-08-07 14:04:06 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-07 14:04:06 +0200 |
| commit | 0d61500c7137f93942a63a356226276c26edfd99 (patch) | |
| tree | f9a9c741f31faf2ceef73c2e0ef8581593019e11 /plugins/syntax/string_notation.ml | |
| parent | 0c6d6b31ad4e52738eb6ee3f62bd8c93ecba8965 (diff) | |
| parent | fc60feb7a3ccd9ec88f6c46929f5fa8172bd7885 (diff) | |
Merge PR #10604: Simplify Lib section handling
Reviewed-by: ejgallego
Reviewed-by: herbelin
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions