# Create a binary distribution. (make.sh should be run first to create
# the various binary files, and make-doc.sh should also be run to
# Create a binary distribution. (make.sh should be run first to create
# the various binary files, and make-doc.sh should also be run to