aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-10-07 11:40:45 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-10-07 11:41:44 +0200
commitd6851cb4ee7d351159f0e3706574b8e384e10650 (patch)
treea5dfb7ec605039304f5d209ced7f5566e8d31d76 /pretyping
parent24f5b8cf170012d43c00d5340173463438905ad2 (diff)
coq_makefile: explicit target install-toploop for toploop plugins
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions