diff options
| author | Théo Zimmermann | 2018-06-22 09:06:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-06-22 09:06:58 +0200 |
| commit | b89904c3831f1ddc02efb2998c71dcaa0df1d286 (patch) | |
| tree | d31b761cb8cb722b14931ef83c1ca0d083a9f4db /dev/ci | |
| parent | 37e8149db7bfa2e7d7fe571b92752f6589101852 (diff) | |
Fix Windows install script following removal of INSTALL.ide and move of INSTALL.doc.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions