aboutsummaryrefslogtreecommitdiff
path: root/.github
diff options
context:
space:
mode:
authorPierre Roux2020-11-11 17:07:14 +0100
committerPierre Roux2020-11-20 19:07:42 +0100
commit1596cdbb2e97f2353236e35fb07be05efe6d1a84 (patch)
treeaa76c9fa00fe7b2999203840041a52e74d7a4032 /.github
parente2f2966c453ecdf788ee1c15d62be68da2cddebe (diff)
Configure default value of -native-compiler
This an implementation of point 2 of CEP coq/ceps#48 https://github.com/coq/ceps/pull/48 Option -native-compiler of the configure script now impacts the default value of the option -native-compiler of coqc. The -native-compiler option of the configure script is added an ondemand value, which becomes the default, thus preserving the previous default behavior. The stdlib is still precompiled when configuring with -native-compiler yes. It is not precompiled otherwise.
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions