aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-11-11 11:20:38 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-11-11 11:31:30 +0100
commit7e992fa784ee6fa48af8a2e461385c094985587d (patch)
tree3109d0608339cb49f24b96ff282709d8c4dab1a7 /tools
parentdd47fcfc08c43288a49797cc72829da3f9642094 (diff)
Coqide: fixing default local links for refman and stdlib.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions