diff src/urweb.grm @ 964:fbc3a0eef45a

Paging mostly working; just need to get it working properly with filtering
author Adam Chlipala <adamc@hcoop.net>
date Sat, 19 Sep 2009 14:21:25 -0400
parents 8e540df3294d
children 10114d7b7477
line wrap: on
line diff
--- a/src/urweb.grm	Sat Sep 19 13:55:37 2009 -0400
+++ b/src/urweb.grm	Sat Sep 19 14:21:25 2009 -0400
@@ -938,7 +938,7 @@
        | eexp PLUS eexp                 (native_op ("plus", eexp1, eexp2, s (eexp1left, eexp2right)))
        | eexp MINUS eexp                (native_op ("minus", eexp1, eexp2, s (eexp1left, eexp2right)))
        | eterm STAR eexp                (native_op ("times", eterm, eexp, s (etermleft, eexpright)))
-       | eexp DIVIDE eexp               (native_op ("div", eexp1, eexp2, s (eexp1left, eexp2right)))
+       | eexp DIVIDE eexp               (native_op ("divide", eexp1, eexp2, s (eexp1left, eexp2right)))
        | eexp MOD eexp                  (native_op ("mod", eexp1, eexp2, s (eexp1left, eexp2right)))
 
        | eexp LT eexp                   (native_op ("lt", eexp1, eexp2, s (eexp1left, eexp2right)))