Thanks for the review, Eli.

> > +@item python execfile ("script-name")
> > +This method is based on the @code{execfile} Python built-in function,
> > +and thus is always available.
> 
> "always" as in "when Python is compiled in", right?

That's correct. But since the documentation was inside the section
dedicated to Python support in GDB, I thought I could get away with
not having to conditionalize this with "when Python is compiled in".
I was going to add a small note, but I think we're already covered:
http://www.sourceware.org/gdb/current/onlinedocs/gdb/Python.html#Python

    23.2 Scripting gdb using Python
    
    You can script gdb using the Python programming language. This feature
    is available only if gdb was configured using --with-python. 

So I did not update the current text in this iteration.  Let me know
if I should and I'll send a new patch shortly after.  For your
convenience, I'm sending an extra diff, which shows the changes
from version 1 to version 2. Since the number of changes is small
compared to the size of the patch, it can be hard to spot these changes.

gdb/doc/ChangeLog:

        * gdb.texinfo (File Options): Adjust the documentation of this
        switch to refer to the "source" command rather than partially
        duplicating some of the relevant information.
        (Extending GDB): Introduce and document the set/show script-extension
        setting.
        (Command Files): Add note explaining that the "source" command
        is also used to evalute scripts written in other languages.
        Remove the short slightly incorrect reference to sourcing Python
        scripts.
        (Python Commands): Document how to execute a Python script from GDB.

Ok to checkin?

Thanks,
-- 
Joel