From: Ben Pfaff <blp@gnu.org>
Date: Thu, 18 Feb 2010 18:53:20 +0000 (-0800)
Subject: remove $build_number from name of directory for building source distribution
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=215d09f8d91f75eac208d4945906a959bc508701;hp=215d09f8d91f75eac208d4945906a959bc508701;p=pspp

remove $build_number from name of directory for building source distribution
---