diff options
| author | Gaëtan Gilbert | 2017-11-24 21:54:48 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-12-14 19:17:49 +0100 |
| commit | 539a62a79f75f9f5190b9bd8edfbb04b880a5f1f (patch) | |
| tree | edaa4550ccc2931682f5a4a8ec038f34630da409 /API/API.ml | |
| parent | 30746e6a9a3296c1aacb2fc03e1c16014232219f (diff) | |
Deprecate dead option Match Strict (ssr).
Diffstat (limited to 'API/API.ml')
0 files changed, 0 insertions, 0 deletions