header files

[Manuel M T Chakravarty]

Ross Paterson <ross at soi.city.ac.uk> wrote,

> In 4.1.1, we have
> 
> 	impent -> " [static] [fname] [&] [cid] "
> 
> so we can specify at most one header file.  How about changing that to
> 
> 	impent -> " [static] {fname} [&] [cid] "
> 
> so we can have any number?  I know this isn't essential (because I can
> create a header file containing #include's) but it would be convenient.

This has been discussed in the past.  The rationale for the
current design is that we cannot provide the full
flexibility of a custom-made C header file anyway; so,
instead of providing a random subset of that functionality,
we provide the bare minimum for people to use the existing
functionality on the C side to achieve whatever is needed.

Cheers,
Manuel