<div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
Date: Wed, 19 Dec 2012 23:16:53 +0100<br>
From: Antoine Musso <<a href="mailto:hashar%2Bwmf@free.fr">hashar+wmf@free.fr</a>><br>
To: <a href="mailto:labs-l@lists.wikimedia.org">labs-l@lists.wikimedia.org</a><br>
Cc: Chris McMahon <<a href="mailto:cmcmahon@wikimedia.org">cmcmahon@wikimedia.org</a>><br>
Subject: [Labs-l] [beta] Fixed up beta earlier today<br>
Message-ID: <<a href="mailto:50D23CD5.4090802@free.fr">50D23CD5.4090802@free.fr</a>><br>
Content-Type: text/plain; charset=ISO-8859-1<br>
<br>
Hello,<br>
<br>
I have fixed up beta earlier today. Some extensions were missing in the<br>
mediawiki/extensions.git repository and were required by our<br>
mediawiki-config configuration files.<br>
<br>
Additionally, the automatic updater was not updating extensions because<br>
of a weird input/output error with a git file :/<br><br></blockquote><div><br></div><div>This is one reason I think we should deploy to beta from Jenkins builds.  For one thing, we would know when they last ran.  For another thing, we would know if they failed.  For another thing, we could make Jenkins do things like run update.php as part of the deploy-to-beta build.  </div>
<div>-Chris </div></div><br>