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 /dev | |
| 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 'dev')
0 files changed, 0 insertions, 0 deletions