move other interface headers to include/
authorBrian Norris <banorris@uci.edu>
Fri, 12 Oct 2012 00:08:20 +0000 (17:08 -0700)
committerBrian Norris <banorris@uci.edu>
Fri, 12 Oct 2012 00:08:20 +0000 (17:08 -0700)
We want all external interface headers (i.e., any #include'd in user
programs) to be in the include/ directory.


No differences found