aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/fake_ide.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-11-21 12:49:17 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-11-21 12:49:17 +0100
commitaa86963464045d61fa0eaf3a7fe67ced7a6a73f4 (patch)
treef1d3e0b213e98e38236bcc3d6f74c80ded896a75 /tools/fake_ide.ml
parent102d2db3ea7a7354de5e019224e2778fe7603b8e (diff)
Remove spurious spaces in merlin file generated by coq_makefile (bug #5213).
Diffstat (limited to 'tools/fake_ide.ml')
0 files changed, 0 insertions, 0 deletions