diff options
Diffstat (limited to 'doc/find_public_interface.sh')
| -rw-r--r-- | doc/find_public_interface.sh | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/doc/find_public_interface.sh b/doc/find_public_interface.sh new file mode 100644 index 000000000..4609846f7 --- /dev/null +++ b/doc/find_public_interface.sh @@ -0,0 +1,20 @@ +#!/bin/bash +# +# Enumerates public interface headers, so that public-only documentation +# can be produced. +# + +cd "$(dirname "$0")" + +echo -n "\"$srcdir/src/include/cvc4.h\" " +echo -n "\"$srcdir/src/include/cvc4_public.h\" " +( (find "$builddir" -name '*.h' | xargs grep -l '^# *include *"cvc4.*_public\.h"'); \ + (find "$srcdir" -name '*.h' | xargs grep -l '^# *include *"cvc4.*_public\.h"'); \ +) | \ +while read f; do + if expr "$f" : ".*_\(template\|private\|test_utils\)\.h$" &>/dev/null; then + continue + fi + echo -n "\"$f\" " +done + |