[slime-devel] filename patch