aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-07-24 15:41:11 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-07-24 15:54:18 +0200
commitd0f9a5523bf16b18bfdf8f427b0e5f005336fa39 (patch)
tree6f58f9d379c67ab71cce020ed15cffa15e40b573 /ide
parent4456b5edc3e2e62624e5251ff1e01dd81fabb29b (diff)
Fixing bug #4265: "coqdep does not handle From ... Require" for good.
Diffstat (limited to 'ide')
0 files changed, 0 insertions, 0 deletions