Skip to content

Move headers in a subdirectory #16

@arthaud

Description

@arthaud

Running sudo make install creates many files in /usr/include.
Some of them have the ap_ prefix which is perfectly fine.
However, some of them have very generic names (box.h, num.h) that could easily clash with other libraries.

I would suggest to create an apron directory in /usr/include and put all the headers there. You could then remove the ap_ prefix for some headers.

Users could then simply #include <apron/xxx.h>.

Thanks!

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions