diff --git a/docs/CompilerDriver.html b/docs/CompilerDriver.html index 9ccf383fae8..4d7cb371dcb 100644 --- a/docs/CompilerDriver.html +++ b/docs/CompilerDriver.html @@ -363,7 +363,8 @@ for. Example:

(switch_option "E", (extern)) ... -

See also the section on plugin priorities.

+

If an external option has additional attributes besides 'extern', they are +ignored. See also the section on plugin priorities.