aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/wg_Detachable.mli
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-10-05 08:22:57 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-10-22 11:57:58 +0200
commit9f8714f4cd3fb59ce38afee48caf081db1919c0c (patch)
tree65861db98cc948443c83d10e54e972fe97414aa5 /ide/wg_Detachable.mli
parent56744aadd413dd9417d245951083117b05170e14 (diff)
Fix incorrect token description for bullets.
Diffstat (limited to 'ide/wg_Detachable.mli')
0 files changed, 0 insertions, 0 deletions