mirror of
https://github.com/genodelabs/genode.git
synced 2024-12-21 06:33:31 +00:00
992a5ec1ae
To raise readability when preparing multiple ports in parallel we prefix also the git clone output with the port name dark-yellow-coloured. To achieve this we sed the git output. In sed \x1b[ resolves to an escape sequence and \033[, that we use normally, doesn't. The echo command, at the other hand, resolves both to an escape sequence. Thus we use the sed-compatible version in general. This commit inhibits the progress output of git clone as it can't be redirected to sed. Ref #1872 |
||
---|---|---|
.. | ||
check_port_arg.inc | ||
check.mk | ||
common.inc | ||
front_end.inc | ||
hash.inc | ||
install.mk | ||
prepare_single_port.mk |