mirror of
https://github.com/nasa/trick.git
synced 2025-03-03 12:24:16 +00:00
PIPESTATUS is only available in bash. For many of the systems we use /bin/sh and /bin/bash are the same, but noooo, not on Ubuntu where it is linked to dash. I set SHELL := /bin/bash in our makefile now.