aboutsummaryrefslogtreecommitdiff
path: root/interp/implicit_quantifiers.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2017-05-30 15:25:45 +0200
committerGaëtan Gilbert2017-05-30 15:25:45 +0200
commit2712ea67dad04faa52871564b79efd1c82127294 (patch)
tree38c7b86542d14d54dce614c0744dd11e69f2282a /interp/implicit_quantifiers.ml
parentfd36c0451c26e44b1b7e93299d3367ad2d35fee3 (diff)
[readlink -f] doesn't work on OSX
We only want an absolute path, no need to follow symlinks.
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions