mirror of
https://git.postgresql.org/git/postgresql.git
synced 2026-04-12 03:47:02 +08:00
Issue noticed while looking at this area of the documentation, for a different patch. This is a matter of style, so no backpatch is done. Discussion: https://postgr.es/m/CAN55FZ0h_YoSqqutxV6DES1RW8ig6wcA8CR9rJk358YRMxZFmw@mail.gmail.com