HEAD has now been tagged as Oct2002RC1, i.e., hugs98/ only (and not fptools/{libraries,hslibs}/ ) --sigbjorn