[slime-devel] #+#. bug report (with fix, maybe)