aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorPierre Letouzey2016-06-07 16:20:40 +0200
committerPierre Letouzey2016-06-07 16:20:40 +0200
commitdd69520b66a3669d9593b59165961baa63d3c40f (patch)
tree8bc3c289b4709efbdeaa03d8156b2c76bfe7700b /ide
parent8df8bc8e3e2aa67f02a83db02fbbe877fa0b0450 (diff)
parentc3698ed4271658fc2edde3870394b3403d7489c9 (diff)
coq_makefile : minor rework
Diffstat (limited to 'ide')
0 files changed, 0 insertions, 0 deletions