If you think it's not a good idea to modify those headers we should
copy them to another location and modify them there. I guess it's
the same.
What? This makes no sense to me.
As we already discussed, Gnulib headers should not be modified in your
source tree (then you can't update them), or installed by make install
(then there are collisions).
If you want to use them in the PDF public headers, then physically
insert them into your headers so there is no file named "gl_list.h" that
gets installed (or modified). Otherwise, just don't use them.
karl
