diff options
| author | Michael Soegtrop | 2018-10-02 11:16:54 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2018-10-02 16:03:15 +0200 |
| commit | a020ede9105662939254ba1296a256fad98c8a3d (patch) | |
| tree | 4a8a2528948fdd80566753322c4e1fa6c38eb7e0 /plugins/syntax/string_syntax.ml | |
| parent | e65d160d5fa4e0b8b5754b0925b0b5a880523bc5 (diff) | |
Fix issue #8611 - Change extensions of log files in WIndows build to _log.txt and _err.txt so that they can be viewed immediately in gitlab
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions