This replaces the tilde character with the string ";SPMtilde;", which
LaTeX2HTML converts to a tilde on output.