mirror of
https://github.com/postgres/postgres.git
synced 2025-11-19 13:42:17 +03:00
380895f2de
Cut out some expensive stuff from the HTML head element that we don't
really need.
This was previously discussed as part of
e8306745e3, but ended up separate because
it changes the output contents slightly.