[slime-devel] [PATCH] (minor bug?)