double get_config_double (string key, double def)
Get a double from a persistent configuration store.
| key | The name of the value to be retrieved. |
| def | The default value (returned if the key has not been previously set). |
| The value associated with key, def if not set. |