Replace double-hyphen ("-‎-") with a dash ("–") like in TeX?

[jgm]

--del-- is a bad idea anyway. -- is far too common in regular typed text, with or without smart typography extensions.