diff options
| author | jp | 2020-02-23 17:45:15 +0000 |
|---|---|---|
| committer | jp | 2020-02-23 17:45:20 +0000 |
| commit | 219f8ef5aec4d6a4f918693bccc9dc548716ea41 (patch) | |
| tree | 6ac926e6a183f4a0b490b5d2b34ded8156aa9297 /src/jib/jib_interactive.mli | |
| parent | 4284ce73ea121b6643cb72823136c4c60518f7ec (diff) | |
set vscode syntax highlighting extension up for publication
Diffstat (limited to 'src/jib/jib_interactive.mli')
0 files changed, 0 insertions, 0 deletions