diff options
| author | Kazuhiko Sakaguchi | 2019-10-24 00:15:13 +0200 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-10-28 17:23:23 +0100 |
| commit | 23a0f7343df0b92f847d7c5c8eec8ab4984295a3 (patch) | |
| tree | 417bb609b58c9e8f4f1934eecc8467b36e5eff12 /doc | |
| parent | e6991dce306c41352c359a8ba5d6d9d6c5e6dfb2 (diff) | |
Rename `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the `coq_makefile` utility
The `coq_makefile` utility and `Makefile`s generated by it generate and include
some files: `<CoqMakefile>.conf`, `<CoqMakefile>.local`, and the dependency file
`.coqdep.d`, where `<CoqMakefile>` is the name of the output file given by the
`-o` option. Out of these, only the name of the dependency file `.coqdep.d` is
fixed to a constant. This seems to be a potential pitfall when we place multiple
`Makefile`s generated by `coq_makefile` in the same directory. This patch
renames `.coqdeps.d` to `.<CoqMakefile>.d`.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/08-tools/10947-coq-makefile-dep.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/08-tools/10947-coq-makefile-dep.rst b/doc/changelog/08-tools/10947-coq-makefile-dep.rst new file mode 100644 index 0000000000..f620b32cb8 --- /dev/null +++ b/doc/changelog/08-tools/10947-coq-makefile-dep.rst @@ -0,0 +1,5 @@ +- 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). |