aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorEnrico Tassi2016-05-19 07:41:09 +0200
committerEnrico Tassi2016-05-19 07:41:09 +0200
commit802366bdf00adf3849499f43ba07ee726da0668a (patch)
treea5d0c160d98a9f414dc670df47ac5840b86506ea /kernel
parentf7fb1918619fcef384d4aa84938246de67c707fa (diff)
coqc: support -o option to specify output file name
The -o option lets one put .vo or .vio files in a directory of choice, i.e. decouple the location of the sources and the compiled files. This ease the integration of Coq in already existing IDEs that handle the build process automatically (eg Eclipse) and also enables one to compile/run at the same time 2 versions of Coq on the same sources. Example: b.v depending on a.v coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions