Re: [PATCHv5 1/5] Scripts to install, delete and clear a MediaWiki

Simon Cathebras [off-list ref] writes:

+function get ($page_name = "") {
+        $curl = curl_init();
+        $page_name_add = "";
+        if ($page_name != "") {
+                $page_name_add = '?page='.$page_name;
+        }
+	$url = $GLOBALS['url'].$page_name_add;
+        $tmp_cookie=$GLOBALS['tmp_cookie'];
+        curl_setopt($curl, CURLOPT_COOKIEJAR, $tmp_cookie);
+        curl_setopt($curl, CURLOPT_RETURNTRANSFER, true);
+        curl_setopt($curl, CURLOPT_FOLLOWLOCATION, true);
+        curl_setopt($curl, CURLOPT_COOKIEFILE, $tmp_cookie);
+        curl_setopt($curl, CURLOPT_HEADER, true);
+        curl_setopt($curl, CURLOPT_URL,$url);
+
+        $page = curl_exec($curl);
+        curl_close($curl);
+        return $page;
+}

Mixed tab/space indentation.

-- 
Matthieu Moy
http://www-verimag.imag.fr/~moy/