From c95512bc5716fc477948ae5e4947afe9dca2976d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 15 Nov 2020 12:26:54 +0100 Subject: Add changelog --- doc/changelog/07-commands-and-options/13352-cep-48.rst | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 doc/changelog/07-commands-and-options/13352-cep-48.rst (limited to 'doc') 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 `_ + (`#13352 `_, + by Pierre Roux). -- cgit v1.2.3