diff options
| author | Tom Lane | 2017-08-11 21:39:27 +0000 |
|---|---|---|
| committer | Tom Lane | 2017-08-11 21:39:27 +0000 |
| commit | d6ecad812f981e6ea611c1022ce7540830393a36 (patch) | |
| tree | b688e908df8f9d01cb13d5b3c1ebdefc48ba9856 /doc/src | |
| parent | 3c8de95979008d67713429d858957c5c78c23d75 (diff) | |
Be more thorough about cleaning out gcov litter.
At least on my machine, a run with code coverage enabled produces some
".gcov" files whose names begin with ".". "rm -f *.gcov" fails to match
those, so they don't get cleaned up by "make clean". Fix it.
Diffstat (limited to 'doc/src')
0 files changed, 0 insertions, 0 deletions