From mboxrd@z Thu Jan 1 00:00:00 1970 From: Martin Pitt Date: Thu, 18 Jul 2013 15:52:48 +0000 Subject: Re: media-player-info 18 release Message-Id: <20130718155248.GJ3023@piware.de> List-Id: References: <20130705050409.GA2946@piware.de> In-Reply-To: <20130705050409.GA2946@piware.de> MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit To: linux-hotplug@vger.kernel.org Tom Gundersen [2013-07-18 16:39 +0200]: > I think you may have forgotten to push this git tag to the public repo? *cough*, thanks for pointing out. That's one of my main pet peeves with git that it doesn't just effing do that with git push. Pushed! Martin -- Martin Pitt | http://www.piware.de Ubuntu Developer (www.ubuntu.com) | Debian Developer (www.debian.org)