1
0
mirror of https://github.com/postgres/postgres.git synced 2025-07-28 23:42:10 +03:00

Doc: restructure documentation of the configure script's options.

The list of configure options has grown long, and there was next
to no organization to it, never mind any indication of which options
were interesting to most people.  Break it into several sub-sections
to provide a bit of structure, and add some introductory text where
it seems helpful to point people to particular options.

I failed to resist the temptation to do a small amount of
word-smithing on some of the option descriptions, too.
But mostly this is reorganization and addition of intro text.

Discussion: https://postgr.es/m/6384.1559917369@sss.pgh.pa.us
This commit is contained in:
Tom Lane
2019-08-30 15:44:00 -04:00
parent 76c2af9266
commit 137b03b862

File diff suppressed because it is too large Load Diff