diff -ur old/urweb/Makefile.in urweb/Makefile.in
--- old/urweb/Makefile.in       2008-10-25 18:18:33.000000000 +0200
+++ urweb/Makefile.in   2008-10-25 21:17:34.000000000 +0200
@@ -32,7 +32,7 @@

 src/urweb.mlb: src/prefix.mlb src/sources src/suffix.mlb
        cat src/prefix.mlb src/sources src/suffix.mlb \
-       | sed 's/^\(.*\).grm$$/\1.mlton.grm.sig\n\1.mlton.grm.sml/' \
+       | sed 's/^\(.*\).grm$$/\1.mlton.grm.sig:\1.mlton.grm.sml/; y/:/\n/' \
        | sed 's/^\(.*\).lex$$/\1.mlton.lex.sml/' \
        >src/urweb.mlb