diff --git a/doc/src/sgml/installation.sgml b/doc/src/sgml/installation.sgml
index 4431ed75a93..182c801bd52 100644
--- a/doc/src/sgml/installation.sgml
+++ b/doc/src/sgml/installation.sgml
@@ -1494,6 +1494,26 @@ su - postgres
+
+ Sometimes it is useful to add compiler flags after-the-fact to the set
+ that were chosen by configure>. An important example is
+ that gcc>'s
+
When developing code inside the server, it is recommended to
@@ -1514,6 +1534,14 @@ su - postgres
+
+
+ The COPT> and PROFILE> environment variables are
+ actually handled identically by the PostgreSQL>
+ makefiles. Which to use is a matter of preference, but a common habit
+ among developers is to use PROFILE> for one-time flag
+ adjustments, while COPT> might be kept set all the time.
+
diff --git a/src/Makefile.global.in b/src/Makefile.global.in
index 59bd7996d18..44bfe28f571 100644
--- a/src/Makefile.global.in
+++ b/src/Makefile.global.in
@@ -582,6 +582,11 @@ ifneq ($(CUSTOM_COPT),)
COPT= $(CUSTOM_COPT)
endif
+#
+# These variables are meant to be set in the environment of "make"
+# to add flags to whatever configure picked. Unlike the ones above,
+# they are documented.
+#
ifdef COPT
CFLAGS += $(COPT)
LDFLAGS += $(COPT)