We are going to use the Makefile to save useful commands without creating too many shell scripts in the top dir.
Jakob Unterwurzacher