'configure-args.delete' bug?

[vincent habchi]

Le 7 déc. 2011 à 17:32, Jeremy Lavergne a écrit :

> Since it involves a space, what does quoting the whole thing you want
> removed do?

Well, bad news: It does not work. If I quote the whole line using double quotes "", nothing gets deleted. If I use simple quotes '', for whatever reason, only the 'if' token gets discarded. So it seems to be a *real* bug.

Vincent