aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/vio_checking.mli
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-29 15:13:13 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-05-30 17:48:04 +0200
commit9b175072b04195d612615c68ff379dd09aa06f0f (patch)
treec4581781f466ad0d026b0f2b66730d2dcc2a8c14 /stm/vio_checking.mli
parent419e7cac23d7b8ac97d46a6c0d3228d591273d2b (diff)
Makefile: $(BEST) controls which coqtop is used to build .vo
This allows to grant a wish by Hugo: to build coqtop.byte and prelude with it, you could do: make -j BEST=byte states
Diffstat (limited to 'stm/vio_checking.mli')
0 files changed, 0 insertions, 0 deletions