From f6637f3955e207ff2243d07e721ae79637a36747 Mon Sep 17 00:00:00 2001 From: Seaswimmer Date: Thu, 1 Aug 2024 13:57:39 -0400 Subject: [PATCH] add CodeMirror extension --- mediawiki/Dockerfile | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/mediawiki/Dockerfile b/mediawiki/Dockerfile index 23b12af..28b2c17 100644 --- a/mediawiki/Dockerfile +++ b/mediawiki/Dockerfile @@ -51,6 +51,10 @@ RUN git clone --depth 1 \ https://gerrit.wikimedia.org/r/mediawiki/extensions/CreateUserPage \ /var/www/html/extensions/CreateUserPage +RUN git clone --depth 1 \ + https://gerrit.wikimedia.org/r/mediawiki/extensions/CodeMirror \ + /var/www/html/extensions/CodeMirror + RUN git clone --depth 1 \ https://gerrit.wikimedia.org/r/mediawiki/extensions/Disambiguator \ /var/www/html/extensions/Disambiguator