diff options
| author | Pierre Roux | 2020-11-15 12:26:54 +0100 |
|---|---|---|
| committer | Pierre Roux | 2020-11-20 19:08:08 +0100 |
| commit | c95512bc5716fc477948ae5e4947afe9dca2976d (patch) | |
| tree | 3ac28b6b6ead5c1faa7b5f15d15d648d9a622ea9 | |
| parent | 673849ed6d0218be566fc9391a77bbed09cb387b (diff) | |
Add changelog
| -rw-r--r-- | doc/changelog/07-commands-and-options/13352-cep-48.rst | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/doc/changelog/07-commands-and-options/13352-cep-48.rst b/doc/changelog/07-commands-and-options/13352-cep-48.rst new file mode 100644 index 0000000000..cb2eeea74b --- /dev/null +++ b/doc/changelog/07-commands-and-options/13352-cep-48.rst @@ -0,0 +1,12 @@ +- **Changed:** + 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. + This an implementation of point 2 of + `CEP #48 <https://github.com/coq/ceps/pull/48>`_ + (`#13352 <https://github.com/coq/coq/pull/13352>`_, + by Pierre Roux). |
