diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-01-12 14:03:47 +0100 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-01-12 14:03:47 +0100 |
commit | 5391d15256af65a0ba0ead4ee6d1ec16f7e362cc (patch) | |
tree | b91db7d25a47898163243957d86a2d259b853866 /lib/aux_file.ml | |
parent | 11bdfe88061c5bda160baec625b862a146809024 (diff) |
Fix configure crash on some version strings of camlp5, e.g. "6.18-exp" (bug #5307).
Diffstat (limited to 'lib/aux_file.ml')
0 files changed, 0 insertions, 0 deletions