aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/session.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-05-22 08:50:36 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-05-22 08:52:31 +0200
commite7043eec55085f4101bfb126d8829de6f6086c5a (patch)
tree041987e27ca681602df21dccfafde0d4b6897500 /ide/session.ml
parent2eb7d2e20a2fc58ae91a5110f26e2f9a3699db46 (diff)
Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X.
Thanks to Vadim Zaliva for testing.
Diffstat (limited to 'ide/session.ml')
0 files changed, 0 insertions, 0 deletions