Function pushExtension

src/cm/mainEditorExtensions.ts:17–20

(target: Extension[], extension?: Extension)

}

function pushExtension(target: Extension[], extension?: Extension): void {
	if (extension == null) return;
	target.push(extension);
}

export const fixedHeightTheme = EditorView.theme({
	"&": { height: "100%" },