Merge pull request #183 from MaRDI4NFDI/user-merge

Add extension UserMerge
MaRDI4NFDI · Feb 14, 2025 · 021c408 · 021c408
2 parents 87a475c + c2cbbf6
commit 021c408
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Dockerfile b/Dockerfile
@@ -65,6 +65,7 @@ bash clone-extension.sh TextExtracts ${WMF_BRANCH};\
 bash clone-extension.sh TimedMediaHandler ${WMF_BRANCH};\
 bash clone-extension.sh Thanks ${WMF_BRANCH};\
 bash clone-extension.sh UniversalLanguageSelector ${WMF_BRANCH};\
+bash clone-extension.sh UserMerge ${REL_BRANCH};\
 bash clone-extension.sh UrlGetParameters ${REL_BRANCH};\
 bash clone-extension.sh VisualEditor ${WMF_BRANCH};\
 bash clone-extension.sh Widgets ${REL_BRANCH};\
@@ -186,6 +187,7 @@ COPY --from=fetcher /TimedMediaHandler /var/www/html/extensions/TimedMediaHandle
 COPY --from=fetcher /Thanks /var/www/html/extensions/Thanks
 COPY --from=fetcher /UniversalLanguageSelector /var/www/html/extensions/UniversalLanguageSelector
 COPY --from=fetcher /UrlGetParameters /var/www/html/extensions/UrlGetParameters
+COPY --from=fetcher /UserMerge /var/www/html/extensions/UserMerge
 COPY --from=fetcher /VisualEditor /var/www/html/extensions/VisualEditor
 COPY --from=fetcher /Widgets /var/www/html/extensions/Widgets
 COPY --from=fetcher /Wikibase /var/www/html/extensions/Wikibase