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 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/changelog/08-tools/10947-coq-makefile-dep.rst b/doc/changelog/08-tools/10947-coq-makefile-dep.rst index f620b32cb8..c59f1312d1 100644 --- a/doc/changelog/08-tools/10947-coq-makefile-dep.rst +++ b/doc/changelog/08-tools/10947-coq-makefile-dep.rst @@ -1,4 +1,5 @@ -- Renamed `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the `coq_makefile` +- **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. |