diff options
| author | Jorge Aparicio <jorge@japaric.io> | 2019-08-21 10:17:27 +0200 |
|---|---|---|
| committer | Jorge Aparicio <jorge@japaric.io> | 2019-08-21 10:17:27 +0200 |
| commit | 07b2b4d83078d0fd260d5f0812e8d5a34d02b793 (patch) | |
| tree | dba2a8e8316e8cd868ccb7b46a80d63c5f61a224 /ci/script.sh | |
| parent | 0e146f8d1142672725b6abb38478f503a9261c80 (diff) | |
doc up
Diffstat (limited to 'ci/script.sh')
| -rw-r--r-- | ci/script.sh | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/ci/script.sh b/ci/script.sh index 1b3d561..11c8d3a 100644 --- a/ci/script.sh +++ b/ci/script.sh @@ -99,13 +99,14 @@ main() { local exs=( idle init - interrupt + hardware + preempt binds resource lock late - static + only-shared-access task message @@ -117,6 +118,7 @@ main() { shared-with-init generics + cfg pool ramfunc ) @@ -160,7 +162,11 @@ main() { fi arm_example "run" $ex "debug" "" "1" - arm_example "run" $ex "release" "" "1" + if [ $ex = types ]; then + arm_example "run" $ex "release" "" "1" + else + arm_example "build" $ex "release" "" "1" + fi done local built=() |