diff options
Diffstat (limited to 'doc/changelog/08-tools/11409-mltop+deprecate_use.rst')
| -rw-r--r-- | doc/changelog/08-tools/11409-mltop+deprecate_use.rst | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/doc/changelog/08-tools/11409-mltop+deprecate_use.rst b/doc/changelog/08-tools/11409-mltop+deprecate_use.rst deleted file mode 100644 index f4f110ed67..0000000000 --- a/doc/changelog/08-tools/11409-mltop+deprecate_use.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Removed:** - The `-load-ml-source` and `-load-ml-object` command line options - have been removed; their use was very limited, you can achieve the same adding - additional object files in the linking step or using a plugin - (`#11409 <https://github.com/coq/coq/pull/11409>`_, by Emilio Jesus Gallego Arias). |