diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 18:45:06 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 18:45:06 +0200 |
| commit | 54063fcda793ca8179047ff2a2c9863891a97acd (patch) | |
| tree | f56d4df99c1bf8bd746ff4bc040567c80732be2e /configure.ml | |
| parent | 5f3954b8d919a8fd89ce2332261698f41bc33550 (diff) | |
| parent | a526ef890f614e130a8afc032d427c81fd8e6442 (diff) | |
Merge PR#753: Fix bug 5026 (the stdlib shouldn't define inconsistent notations).
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions