mirror of
https://github.com/genodelabs/genode.git
synced 2024-12-22 23:12:24 +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 |
||
---|---|---|
.. | ||
mk | ||
check_port_source | ||
current | ||
list | ||
prepare_port | ||
shortcut | ||
update_hash |