aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorHugo Herbelin2015-01-29 11:48:36 +0100
committerHugo Herbelin2015-02-04 19:58:59 +0100
commite07bce3fa05838c4cd826d1b4349604014705208 (patch)
tree77c4abd9ba35f448f74dc844bfb05d6f3c299129 /dev
parent9347618755eed17d683f590f8bd9c47aacfcfa17 (diff)
Detecting automatically whether .opt versions of ocaml executables exist;
making configure option -opt deprecated.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions