diff options
| author | Gaëtan Gilbert | 2020-02-21 13:24:53 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-21 13:24:53 +0100 |
| commit | e1f2a1b97bb61e9c5ebaffda55a3be1ea3267c6b (patch) | |
| tree | f4c205e5d98700c0b118efe09498e22aff44adfb /doc | |
| parent | 4b6e6c6c187441f928921cbdd14093e296682f40 (diff) | |
| parent | 7489014fa6053c28e09852b0bf0602f2160cdda5 (diff) | |
Merge PR #11617: [init] Add `-boot` option to avoid binding `Coq.` prefix.
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: herbelin
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/07-commands-and-options/11617-toplevel+boot.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst b/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst new file mode 100644 index 0000000000..49dd0ee2d8 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst @@ -0,0 +1,5 @@ +- **Added:** + New ``coqc`` / ``coqtop`` option ``-boot`` that will not bind the + `Coq` library prefix by default + (`#11617 <https://github.com/coq/coq/pull/11617>`_, + by Emilio Jesus Gallego Arias). |