diff options
| author | Hugo Herbelin | 2019-05-27 17:23:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-06-08 12:02:25 +0200 |
| commit | 6f05a46e08fdb8de2319c36f07a737b1acebfe31 (patch) | |
| tree | f3dd72ed18d47a95996bc2bc06d8ba87db1d128d | |
| parent | 08a32f04b77b29ad17db75f7ba98c122c31b96aa (diff) | |
Updated changelog.
| -rw-r--r-- | doc/changelog/08-tools/10245-require-command-line.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/08-tools/10245-require-command-line.rst b/doc/changelog/08-tools/10245-require-command-line.rst new file mode 100644 index 0000000000..54417077f5 --- /dev/null +++ b/doc/changelog/08-tools/10245-require-command-line.rst @@ -0,0 +1,6 @@ +- Add command line options `-require-import`, `-require-export`, + `-require-import-from` and `-require-export-from`, as well as their + shorthand, `-ri`, `-re`, `-refrom` and -`rifrom`. Deprecate + confusing command line option `-require` + (`#10245 <https://github.com/coq/coq/pull/10245>`_ + by Hugo Herbelin, review by Emilio Gallego). |