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