diff options
| author | Emilio Jesus Gallego Arias | 2020-03-12 19:06:22 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-12 19:06:22 -0400 |
| commit | c9953e36ef380916ee805b8550439868e615921c (patch) | |
| tree | 04335495a0be010e1eda2dcd4f1c957cd2f8b380 /plugins/syntax/string_notation.mli | |
| parent | 1a7cdc1da9bff2e46acdd5c07a7eee5dcd27d731 (diff) | |
[ci] [doc] Point to actual docker instructions.
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions