aboutsummaryrefslogtreecommitdiffhomepage
path: root/INSTALL.ide
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-06-09 23:24:57 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-06-16 18:21:08 +0200
commit2194292dbe88674fd9a606bb22f28d332f670f77 (patch)
tree21c2e91b13a5de21856554b17f5dfaa61101e253 /INSTALL.ide
parentaf7a9a4e44739968b68aeb1cb0a1f70a1aa34e88 (diff)
Revise syntax of Hint Cut
As noticed by C. Cohen it was confusingly different from standard notation.
Diffstat (limited to 'INSTALL.ide')
0 files changed, 0 insertions, 0 deletions