>Shouldn't this be a `defcustom'?  It seems like an option a user might
>want to customize.

good idea,  updated.