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