diff options
| -rw-r--r-- | modules/mediawiki/files/init_wiki.php | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/modules/mediawiki/files/init_wiki.php b/modules/mediawiki/files/init_wiki.php index 926c52fc..a0e3a520 100644 --- a/modules/mediawiki/files/init_wiki.php +++ b/modules/mediawiki/files/init_wiki.php @@ -2,6 +2,10 @@ $wiki_root = $argv[1]; $mw_root = '/usr/share/mediawiki'; +if (!is_dir("$wiki_root/config")) { + exit(1); +} + // DefaultSettings.php complain if not defined define('MEDIAWIKI',1); |