Re: clisp: Fix collision between ASCII character names and Unicode c...

[Bruno H. <br...@cl...>]

Hi Sam,

> When changing docbook files, please do "make -C doc check" to ensure you
> did not break anything.

Thanks for fixing it up.

So that I have this command readily available, I'm adding a target for it
in Makefile.devel.

Bruno