Merge pull request #398 from MaRDI4NFDI/edit-code

Enable extensions to edito code
MaRDI4NFDI · Sep 27, 2023 · 885b378 · 885b378
2 parents 24c7fe3 + 9e05b0b
commit 885b378
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/mediawiki/LocalSettings.d/CodeEditingExtension.php b/mediawiki/LocalSettings.d/CodeEditingExtension.php
@@ -0,0 +1,7 @@
+<?php
+wfLoadExtension( 'JsonConfig' );
+wfLoadExtension( 'CodeEditor' );
+$wgDefaultUserOptions['usebetatoolbar'] = 1; // user option provided by WikiEditor extension
+wfLoadExtension( 'CodeMirror' );
+// Enables use of CodeMirror by default but still allow users to disable it
+$wgDefaultUserOptions['usecodemirror'] = 1;