Just a small bump. The new version (0.8.0, still beta) of the shell arrived 
today. It contains the option to quit from the shell with Ctrl-D too. Better 
late than never. :)

Reply via email to