Remove <nodeputy.h> from default flags
Summary:
Deputy annotations [1] can be used to label safety properties. They are
used extensively in the kernel, but in user-space there is only one use.
The macros have short names (like 'COUNT', 'SAFE') which can conflict
when building other applications. Furthermore, these are not being
checked and are just stripped during the build.
Note: the change to <kernel.h> is needed because it is included from a
generated file:
build-x86_64/capabilities/cap_predicates.c
[1] http://ivy.cs.berkeley.edu/ivywiki/uploads/deputy-manual.html
Test Plan: `make clean && make` was successful
Differential Revision: https://code.systems.ethz.ch/D6
projects / barrelfish / commit