[bug-gawk] Description of the option --disable-extensions

[М]

For some reason I have to compile GNU AWK with a completely disabled API for 
extensions.
When analysing the ./configure help, I supposed that the option 
--disable-extensions was what I'd been looking for.

$ sh ./configure --help
`configure' configures GNU Awk 5.0.0 to adapt to many kinds of systems.
...
--disable-extensions    disable dynamic extensions (default is detect)
...


Such an option is quite common, with a usual behavior.
And I was glad to notice that the string "API: 2.0" disappeared from the 
--version output:

$ sh ./configure --disable-extensions --prefix=/path/to/
...
$ make
...
$ make install
...
$ /path/to/bin/gawk --version
GNU Awk 5.0.0 (GNU MPFR 4.0.1, GNU MP 6.1.2)
Copyright (C) 1989, 1991-2019 Free Software Foundation.
...


But I fell into doubts after reading the corresponding description in the 
manual:

B.2.3 Additional Configuration Options
...
--disable-extensions
Disable configuring and building the sample extensions in the extension direc-
tory. This is useful for cross-compiling. The default action is to dynamically
check if the extensions can be configured and compiled.
...


That is, it states that this option refers only to the sample extensions 
provided with the GNU AWK distribution.
Nothing about user extensions, which can be compiled (and used?) after that.

If the option --disable-extensions is passed to ./configure, will the final 
interpreter raise an error
when a user tries to load some extensions in a script? What is the proper 
behavior?
Or this description in the manual is ambiguous/incorrect?

_______________

Yours respectfully,
Mark Krauze