diff --git a/stdout.sh b/stdout.sh new file mode 100755 index 0000000..2da244b --- /dev/null +++ b/stdout.sh @@ -0,0 +1,12 @@ +#!/bin/sh + +# A trivial script that takes an output file as the first argument, an +# executable as the second, and subsequent arguments. stdout is piped to the +# output file. +# +# This is used to workaround CMake's inflexible output options for custom +# targets. + +dst=$1 +shift 1 +exec $@ > $dst