aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.doc
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-12-05 13:39:13 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-14 15:39:28 +0100
commit20916bd558a355b597337101e3281bb5ebbfcd36 (patch)
tree06946e7bb2f8928872ae4e18c945e7c3443dca8d /Makefile.doc
parentd2fb531761e1f4fa02d0c7e7b5b51febe48e357e (diff)
detype_case predicate is not optional
Diffstat (limited to 'Makefile.doc')
0 files changed, 0 insertions, 0 deletions