The JSExtension class now has a get_settings method that returns, by

default, the associated extension's settings. This method can be

overrided by subclasses to provide different settings at initialization

time.