diff jslib/urweb.js @ 584:101eb0058136

Used an option as a source
author Adam Chlipala <adamc@hcoop.net>
date Thu, 01 Jan 2009 10:49:42 -0500
parents 66463006f893
children 35471f067980
line wrap: on
line diff
--- a/jslib/urweb.js	Thu Jan 01 10:18:20 2009 -0500
+++ b/jslib/urweb.js	Thu Jan 01 10:49:42 2009 -0500
@@ -42,3 +42,4 @@
 }
 
 function ts(x) { return x.toString() }
+function pf() { alert("Pattern match failure") }