diff options
| author | Pierre Schmitz <pierre@archlinux.de> | 2008-03-21 11:49:34 +0100 |
|---|---|---|
| committer | Pierre Schmitz <pierre@archlinux.de> | 2008-03-21 11:49:34 +0100 |
| commit | 086ae52d12011746a75f5588e877347bc0457352 (patch) | |
| tree | e73263c7a29d0f94fafb874562610e16eb292ba8 /includes/Namespace.php | |
| parent | 749e7fb2bae7bbda855de3c9e319435b9f698ff7 (diff) | |
Update auf MediaWiki 1.12.0
Diffstat (limited to 'includes/Namespace.php')
| -rw-r--r-- | includes/Namespace.php | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/includes/Namespace.php b/includes/Namespace.php index f4df3bac..57a71282 100644 --- a/includes/Namespace.php +++ b/includes/Namespace.php @@ -41,6 +41,11 @@ if( is_array( $wgExtraNamespaces ) ) { * Users and translators should not change them * */ + +/* +WARNING: The statement below may fail on some versions of PHP: see bug 12294 +*/ + class Namespace { /** |