diff options
| author | Théo Zimmermann | 2020-03-29 22:12:47 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-30 12:24:43 +0200 |
| commit | 431541f91a09e9d8fe3b027475975a771d93332a (patch) | |
| tree | 5945984aa6e04ffa39b2d90cddc12f66a1eecd84 /plugins/syntax/string_notation.mli | |
| parent | 7ff44dd02d935cb078487629b342b7106cc72955 (diff) | |
[dune] [docgram] Remove bash hack thanks to new option -no-update.
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions