From 23a0f7343df0b92f847d7c5c8eec8ab4984295a3 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 24 Oct 2019 00:15:13 +0200 Subject: Rename `VDFILE` from `.coqdeps.d` to `..d` in the `coq_makefile` utility The `coq_makefile` utility and `Makefile`s generated by it generate and include some files: `.conf`, `.local`, and the dependency file `.coqdep.d`, where `` 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 `..d`. --- doc/changelog/08-tools/10947-coq-makefile-dep.rst | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 doc/changelog/08-tools/10947-coq-makefile-dep.rst (limited to 'doc') 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 `..d` in the `coq_makefile` + utility, where `` 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 `_, by Kazuhiko Sakaguchi). -- cgit v1.2.3