diff options
| author | Matthieu Sozeau | 2017-08-31 17:22:33 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2017-08-31 17:22:56 +0200 |
| commit | 06b871974ae222f878142c8cab03fd52d4511895 (patch) | |
| tree | 1deafb887d1eca4a1c15a5727648400a4ff909ec /plugins/syntax/string_syntax.ml | |
| parent | bdaf7032912feabf5ee97af33bf32e4359ad2d25 (diff) | |
RefMan-ssr: fix warning
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions