webstdin: Redirect stdin from `/dev/tty`

The script is usually run with stdin redirected from a file or a pipe.
It's necessary to re-redirect stdin so that a console browser
reads from the terminal.

diff --git a/bin/webstdin b/bin/webstdin
index 395456ccd9a5aa8daf6ac11b81aa0d154cbab00f..209cecfef0748a347fb383350870f45536cd2788 100755 (executable)
--- a/bin/webstdin
+++ b/bin/webstdin
@@ -13,4 +13,4 @@ done
 shift `expr $OPTIND - 1`
 
 tmpfile="`mktemp -t XXXXXX.$ext`" && cat - >"$tmpfile" &&
-webbrowser $new_win file://"$tmpfile" && (sleep 10 && exec rm "$tmpfile" &)
+webbrowser $new_win file://"$tmpfile" </dev/tty && (sleep 10 && exec rm "$tmpfile" &)