diff options
Diffstat (limited to 'doc/changelog/08-tools/10947-coq-makefile-dep.rst')
| -rw-r--r-- | doc/changelog/08-tools/10947-coq-makefile-dep.rst | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/doc/changelog/08-tools/10947-coq-makefile-dep.rst b/doc/changelog/08-tools/10947-coq-makefile-dep.rst deleted file mode 100644 index c59f1312d1..0000000000 --- a/doc/changelog/08-tools/10947-coq-makefile-dep.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - Renamed `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the `coq_makefile` - utility, where `<CoqMakefile>` is the name of the output file given by the - `-o` option. In this way two generated makefiles can coexist in the same - directory. - (`#10947 <https://github.com/coq/coq/pull/10947>`_, by Kazuhiko Sakaguchi). |