From: Ben Pfaff <blp@gnu.org>
Date: Thu, 18 Feb 2010 18:36:16 +0000 (-0800)
Subject: save distributed files to Git when we build binary, not source
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=ce89fa1471dad1b99a8b8f6bff68c74bf27299b0;hp=ce89fa1471dad1b99a8b8f6bff68c74bf27299b0;p=pspp

save distributed files to Git when we build binary, not source
---