aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorEnrico Tassi2017-09-04 15:37:00 +0200
committerEnrico Tassi2017-09-07 12:48:18 +0200
commit6729388e9f51d7efb86ac64d10cc3eb4fffe44a0 (patch)
treee1b01250d7ca70490f483136e63d0490b54439ed /plugins
parentcb2d69efa4d012a6828077675aba1d2a51d710ef (diff)
dev/build/windows/makecoq_mingw.sh: install camlp5's META file
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions