aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/obligations.mli
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-11-23 17:06:37 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-11-23 17:06:37 +0100
commit1dfa6c551d95a82c242a514b81dd8cfac6f478d3 (patch)
tree35cbe29e864f81fafffc4d2df3a4277be77e4056 /vernac/obligations.mli
parent22ae762fa8940028f6a3d8a5fd4147d5ca3b53b9 (diff)
Fix link to Recursive Make Considered Harmful
Diffstat (limited to 'vernac/obligations.mli')
0 files changed, 0 insertions, 0 deletions