diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-29 15:13:13 +0200 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-29 15:13:20 +0200 |
commit | 073178a9821d10b72fe581d3ba7814afd7dfbb05 (patch) | |
tree | abe35dae9e5fe37bc3ec9814babd67787dfe5787 /.gitattributes | |
parent | dd134de0b068c70adb80c94921673086f0002c30 (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 '.gitattributes')
0 files changed, 0 insertions, 0 deletions