--- a/doc/makefile-variables.txt Thu Apr 11 09:31:09 2013 -0700
+++ b/doc/makefile-variables.txt Thu Apr 11 10:40:20 2013 -0700
@@ -89,3 +89,8 @@
default is "/usr"; set it if some other value (e.g., "/usr/gnu") is needed.
* CONFIGURE_SCRIPT should be set if the default "$(SOURCE_DIR)/configure" is
unsuitable for whatever reason.
+
+* studio_OPT has a default value of "-xO4". Occasional bugs in the optimizer
+ have been found which have required altering this to "-xO3". There are also
+ studio_OPT.$(MACH).$(BITS) versions of this available if greater specificity
+ is needed.