From 9eb80b1f9f2dfef4eaddf0d6233349da92310d77 Mon Sep 17 00:00:00 2001
From: Moritz Schubotz <github@ckurs.de>
Date: Wed, 27 Sep 2023 16:12:35 +0200
Subject: [PATCH] Fix: Disable CodeEditor

---
 mediawiki/LocalSettings.d/CodeEditingExtension.php | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mediawiki/LocalSettings.d/CodeEditingExtension.php b/mediawiki/LocalSettings.d/CodeEditingExtension.php
index 00eea47..61903c4 100644
--- a/mediawiki/LocalSettings.d/CodeEditingExtension.php
+++ b/mediawiki/LocalSettings.d/CodeEditingExtension.php
@@ -1,6 +1,6 @@
 <?php
 wfLoadExtension( 'JsonConfig' );
-wfLoadExtension( 'CodeEditor' );
+//wfLoadExtension( 'CodeEditor' ); requires wiki editor that is not yet availible.
 $wgDefaultUserOptions['usebetatoolbar'] = 1; // user option provided by WikiEditor extension
 wfLoadExtension( 'CodeMirror' );
 // Enables use of CodeMirror by default but still allow users to disable it