diff options
| author | Enrico Tassi | 2020-12-01 17:02:20 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2020-12-03 16:03:37 +0100 |
| commit | 73eb97c9067caabe5dc93bbb4c5e68b5783f1787 (patch) | |
| tree | 733942ae03de8cf524c1ed033257906998986472 /doc/sphinx/changes.rst | |
| parent | 002ab0b6bdf38c4dea0ce74e2a0df1e3d2bc238d (diff) | |
Apply suggestions from code review
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'doc/sphinx/changes.rst')
| -rw-r--r-- | doc/sphinx/changes.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 6facb0e207..9a2e1b686b 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -83,7 +83,7 @@ Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin, Vincent Laporte, Assia Mahboubi, Kenji Maillard, Guillaume Melquiond, Pierre-Marie Pédrot, Clément Pit-Claudel, Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico -Tassi, Laurent Théry, Anton Trunov, Li-yao Xia, Théo Zimmermann +Tassi, Laurent Théry, Anton Trunov, Li-yao Xia and Théo Zimmermann The 52 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric Besson, Lasse Blaauwbroek, Clément Blaudeau, Martin Bodin, Ali Caglayan, Tej Chajed, @@ -535,8 +535,8 @@ Commands and options `-native-compiler` option of the configure script is added as an on demand 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. + 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>`_, |