# Shell script to build Makefile in a build directory. It must be called
# from inside the directory. It does its own checking of when to rebuild; it
# Shell script to build Makefile in a build directory. It must be called
# from inside the directory. It does its own checking of when to rebuild; it