diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-07-06 12:48:02 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-07-06 12:48:02 +0200 |
| commit | 0387d0c1cca76dbcc6a55aadb3198e4868a83112 (patch) | |
| tree | fd66589ba8f73ad669935d0259a8113240eb37b2 /configure.ml | |
| parent | fd72a9c257f22a7c66990fb9152b43ba088d9a47 (diff) | |
| parent | f6701cffa04c0df25634ad60004fbfcf4ca422ec (diff) | |
Merge remote-tracking branch 'github/pr/199' into v8.5
Was PR#199: Unbreak singleton list-like notation (-compat 8.4)
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions