diff options
| -rwxr-xr-x | tools/ci-build | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/ci-build b/tools/ci-build index f618a2da5e..de96090ebe 100755 --- a/tools/ci-build +++ b/tools/ci-build @@ -19,6 +19,7 @@ # 2. for windows, directory in which to build (trunk, 4.02, etc) # 3. options: # -conf configure-option +# -patch1 file-name apply patch with -p1 error () { echo "$1" >&2 @@ -63,6 +64,7 @@ shift 2 while [ $# -gt 0 ]; do case $1 in -conf) confoptions="$confoptions $2"; shift 2;; + -patch1) patch -f -p1 <"$2"; shift 2;; *) error "unknown option $1";; esac done |