[m-rev.] for review: save the commit id in srcdist packages

[Julien Fischer]

For review by anyone.

Any preferences as to the name of the file?

-------------------------------------------

Save the commit id in srcdist packages.

tools/build_srcdist:
     Save the git commit id a srcdist is based upon in a file
     within that srcdist.

diff --git a/tools/build_srcdist b/tools/build_srcdist
index 45bda43..ffd21ba 100755
--- a/tools/build_srcdist
+++ b/tools/build_srcdist
@@ -103,6 +103,7 @@ UNBOXED_FLOATS=no
  # git checkout -- VERSION
  git submodule deinit -f .
  git clean -d -f -x
+git rev-parse HEAD > COMMIT_ID
  if [ -n "$RELEASE_VERSION" ]; then
      sed "s/VERSION=.*/VERSION=$RELEASE_VERSION/" VERSION > VERSION.new
      mv VERSION.new VERSION