On Sat, 12 Nov 2011 13:24:40 -0800, Jameson Graef Rollins <jrollins@finestructure.net> wrote: > On Sat, 12 Nov 2011 23:07:38 +0200, Tomi Ollila <tomi.ollila@iki.fi> wrote: > > 1) add line > > { echo QUIT > /dev/tcp/127.0.0.1/25025; } 2>/dev/null > > I have no directory called "/dev/tcp" on my system. > You shouldn't. See (info "(bash)Redirections") : #+begin_quote Bash handles several filenames specially when they are used in redirections, as described in the following table: [...] `/dev/tcp/HOST/PORT' If HOST is a valid hostname or Internet address, and PORT is an integer port number or service name, Bash attempts to open a TCP connection to the corresponding socket. [...] #+end_quote > jamie. > _______________________________________________ > notmuch mailing list > notmuch@notmuchmail.org > http://notmuchmail.org/mailman/listinfo/notmuch Peace -- Pieter