aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-07-28 15:42:47 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-07-28 15:42:47 +0200
commit75d7504269c1275bebae78aec7f116114a05c153 (patch)
tree1bf6a03e3378e6ad013d0b31e1e26ad0b571ebdb /engine
parent2a7ba998bf7d2c461fdbd8b710b7124395bafaa2 (diff)
Fix documentation of Hint Mode (bug #4911).
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions