michael@0: function f() {
michael@0:     "" < "";
michael@0: }