diff options
author | Michael Schwarz <michi.schwarz@gmail.com> | 2014-12-04 00:40:56 +0100 |
---|---|---|
committer | Michael Schwarz <michi.schwarz@gmail.com> | 2014-12-04 00:40:56 +0100 |
commit | f61385332843af3100f990335e03c583e980d34e (patch) | |
tree | cb75220506005145766bcb6aa91837150cbfacfb | |
parent | 27db6e19926c5074e638d36ca807886dfef6f12d (diff) | |
download | pogojig-f61385332843af3100f990335e03c583e980d34e.tar.gz pogojig-f61385332843af3100f990335e03c583e980d34e.tar.bz2 pogojig-f61385332843af3100f990335e03c583e980d34e.zip |
Easier way to specify how files are generated.
-rwxr-xr-x | generate_sources.sh | 27 |
1 files changed, 20 insertions, 7 deletions
diff --git a/generate_sources.sh b/generate_sources.sh index 687f91a..2d33554 100755 --- a/generate_sources.sh +++ b/generate_sources.sh @@ -1,9 +1,22 @@ #! /usr/bin/env bash -if [ "$1" ]; then - # Print the content of the generated source named $1 here. - true -else - # Print a list of names of the files that should be generated using this script here. - true -fi +set -e -o pipefail + +current_file_name=$1 + +# This function should be called for each generated file with the file's name as the first argument and the command to call to produce the file's content as the remaining arguments. +function generate_file() { + file_name=$1 + shift + generate_command=("$@") + + if ! [ "$current_file_name" ]; then + echo "$file_name" + elif [ "$current_file_name" == "$file_name" ]; then + "${generate_command[@]}" + fi +} + +# Call generate_file for each file to be generated. +# E.g.: +# generate_file src/test.scad echo "cube();" |