2023-07-09 10:47:05 +00:00
|
|
|
import {getCurrentExtension, setExtensionManager} from './sharedInternals.js';
|
2023-07-01 00:11:37 +00:00
|
|
|
|
|
|
|
export {
|
|
|
|
getSettings,
|
|
|
|
initTranslations,
|
|
|
|
gettext,
|
|
|
|
ngettext,
|
|
|
|
pgettext
|
|
|
|
} from './sharedInternals.js';
|
|
|
|
|
2023-07-10 03:12:30 +00:00
|
|
|
const {extensionManager} = imports.ui.main;
|
2023-07-09 10:47:05 +00:00
|
|
|
setExtensionManager(extensionManager);
|
2023-07-10 03:12:30 +00:00
|
|
|
|
2023-07-01 00:11:37 +00:00
|
|
|
/**
|
|
|
|
* Open the preference dialog of the current extension
|
|
|
|
*/
|
|
|
|
export function openPrefs() {
|
|
|
|
const extension = getCurrentExtension();
|
|
|
|
|
|
|
|
if (!extension)
|
|
|
|
throw new Error('openPrefs() can only be called from extensions');
|
|
|
|
|
2023-07-10 03:12:30 +00:00
|
|
|
extensionManager.openExtensionPrefs(extension.uuid, '', {});
|
2023-07-01 00:11:37 +00:00
|
|
|
}
|