Merge pull request #128 from wikimedia/rm-dev

Remove unused dev/ folder
wikimedia · Jul 15, 2023 · 62d1870 · 62d1870
2 parents d9637c7 + 1ccf36d
commit 62d1870
Show file tree

Hide file tree

Showing 5 changed files with 0 additions and 522 deletions.
diff --git a/dev/Dockerfile b/dev/Dockerfile
diff --git a/dev/README.md b/dev/README.md
diff --git a/dev/apache/mediawiki.conf b/dev/apache/mediawiki.conf