diff src/sources @ 957:2831be2daf2e

Grid changed to use Dlist.replace; filters stopped working
author Adam Chlipala <adamc@hcoop.net>
date Thu, 17 Sep 2009 19:01:04 -0400
parents e6070333d8a8
children dfe34fad749d
line wrap: on
line diff
--- a/src/sources	Thu Sep 17 17:17:49 2009 -0400
+++ b/src/sources	Thu Sep 17 19:01:04 2009 -0400
@@ -131,6 +131,9 @@
 rpcify.sig
 rpcify.sml
 
+tailify.sig
+tailify.sml
+
 tag.sig
 tag.sml