diff options
| author | Gaëtan Gilbert | 2020-05-18 10:54:15 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-29 16:41:19 +0200 |
| commit | 083ab9fb9ac3b63d741e342cfb2a847968a6784e (patch) | |
| tree | 4b247e2e146c84459b4a6f151957e193e86dc85d /ide/wg_ScriptView.ml | |
| parent | d75b889948fbfd5600d505ab823a0e6da2195af6 (diff) | |
Require in Section: warning is now about fragility not deprecation.
Diffstat (limited to 'ide/wg_ScriptView.ml')
0 files changed, 0 insertions, 0 deletions