aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorSigurd Schneider2017-07-20 18:33:46 +0200
committerSigurd Schneider2017-08-07 11:44:35 +0200
commit0e7e6953e9ee4178d48bf7fa05a7f03d13aa4a6f (patch)
treea0449928105e302978093b189ceeb96470a94f64 /plugins
parent1f46ff6db53c2ca471d9ea067d0824755b2f34da (diff)
Add build_coq_or to API
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions