diff options
| author | Maxime Dénès | 2018-10-30 13:08:22 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-30 13:11:30 +0100 |
| commit | 6c4e4b9fc63b3282422024d556a644adc55b13f6 (patch) | |
| tree | cfb10d1f6061bc3a366257d49756f8992114cff7 /plugins/syntax/string_syntax.ml | |
| parent | 1b35eebd0ac45233ec1714a4040eddedf0d656f5 (diff) | |
Remove fully_empty_glob_sign which uses a dummy environment
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions