diff options
| author | Théo Zimmermann | 2018-10-01 11:49:57 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-01 11:49:57 +0200 |
| commit | cce3f57a9f0299e9010ea5af666f8e9e7055fc34 (patch) | |
| tree | 2256e0d839477a69430597a8350d35c8865c27c9 /plugins/syntax/string_syntax.ml | |
| parent | c155259dee7e4b2bfafe42375b45f2f4d6c6cfbd (diff) | |
| parent | e8b7c1bd1e4e6a1ac005b5eb299d0ef946b83c96 (diff) | |
Merge PR #8604: Fix issue 8603 Move Windows CI runs to folder C:/ci
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions