Fabian Homborg 4a47e212f8 Color the default prompt host if running via SSH ... This is part of our (well, my) quest to spice up the default prompt. In this case we color the host if $SSH_TTY is set, which is easy to detect and helps draw attention to the host. See #6398. See #6375.		2019-12-30 14:03:36 +01:00
..
web_config	Color the default prompt host if running via SSH	2019-12-30 14:03:36 +01:00
create_manpage_completions.py	Reformat all files	2019-05-05 12:09:25 +02:00
deroff.py	Fix: equality vs identity	2019-11-06 14:13:21 +08:00