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 | ||