diff options
| author | Tom Lane | 2021-08-08 19:35:30 +0000 |
|---|---|---|
| committer | Tom Lane | 2021-08-08 19:35:30 +0000 |
| commit | c905e64d42fe0725ab7fe84b70a41b4c381aee07 (patch) | |
| tree | 6bb0049cc904c77a0b54684d45ddbe70594e20e5 /src/tools/git-external-diff | |
| parent | 5227d99896726b3c889e388f14a3593e104e36ee (diff) | |
Doc: remove bogus <indexterm> items.
Copy-and-pasteo in 665c5855e, evidently. The 9.6 docs toolchain
whined about duplicate index entries, though our modern toolchain
doesn't. In any case, these GUCs surely are not about the
default settings of these values.
Diffstat (limited to 'src/tools/git-external-diff')
0 files changed, 0 insertions, 0 deletions