diff options
Diffstat (limited to 'scripts/gen_build_files.sh')
-rwxr-xr-x | scripts/gen_build_files.sh | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/scripts/gen_build_files.sh b/scripts/gen_build_files.sh index ebee17c64..f79fa2f83 100755 --- a/scripts/gen_build_files.sh +++ b/scripts/gen_build_files.sh | |||
@@ -20,7 +20,9 @@ chk() { status "CHK" "$@"; } | |||
20 | generate() | 20 | generate() |
21 | { | 21 | { |
22 | # NB: data to be inserted at INSERT line is coming on stdin | 22 | # NB: data to be inserted at INSERT line is coming on stdin |
23 | local src="$1" dst="$2" header="$3" | 23 | src="$1" |
24 | dst="$2" | ||
25 | header="$3" | ||
24 | #chk "${dst}" | 26 | #chk "${dst}" |
25 | { | 27 | { |
26 | # Need to use printf: different shells have inconsistent | 28 | # Need to use printf: different shells have inconsistent |