diff options
| author | Mike Vink <mike1994vink@gmail.com> | 2023-04-23 22:37:39 +0200 |
|---|---|---|
| committer | Mike Vink <mike1994vink@gmail.com> | 2023-04-23 22:37:39 +0200 |
| commit | 9ea275a2e72fb7eee38d32be2f955a2a05ced682 (patch) | |
| tree | cb13777d37996073fcb6e0eeb3dd2dedc0b115ee /shell-scripts | |
| parent | cb008d4380a8f9d0dba43761155d5cd85f7f1181 (diff) | |
fixup
Diffstat (limited to 'shell-scripts')
| -rw-r--r-- | shell-scripts/compile | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/shell-scripts/compile b/shell-scripts/compile index 61ce9a9..8e74ffa 100644 --- a/shell-scripts/compile +++ b/shell-scripts/compile @@ -7,9 +7,14 @@ error () { } case "${@}" in + racket*) + shift + echo " \-> racket -l errortrace -t ${@}" + racket -l errortrace -t ${@} + ;; ansible-lint*) - echo " \-> ansible-lint" shift + echo " \-> ansible-lint --profile production --write=all -qq --nocolor" ansible-lint --profile production --write=all -qq --nocolor ${@} ;; awx*) |