diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-02-27 14:04:18 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-02-27 14:04:18 +0000 |
| commit | c3662482d3d9f4bda5f5d0e92f1b2367954b8af3 (patch) | |
| tree | 8f481539f6d10911225c5ec3653b3079b8184324 /ide/utils/configwin.mli | |
| parent | e3124e098ef8170dac2b348b91757a7034bc4999 (diff) | |
[stdlib] move “Require” out of sections
Diffstat (limited to 'ide/utils/configwin.mli')
0 files changed, 0 insertions, 0 deletions