Francisco 5e7ee01755
Merge pull request #14345 from HendrikVE/pr/shell-exit-on-ctrl-d
sys/shell: terminate shell on Ctrl-D
2020-10-22 09:25:13 +02:00
..
2020-10-21 17:40:44 +02:00