# This script is used to turn one or more of the "patch/*" branches
# into one or more diffs in the "patches" directory. Pass the option
# --gen if you want generated files in the diffs. Pass the name of
# This script is used to turn one or more of the "patch/*" branches
# into one or more diffs in the "patches" directory. Pass the option
# --gen if you want generated files in the diffs. Pass the name of