summaryrefslogtreecommitdiff
path: root/src/include
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2020-11-19 11:30:52 -0800
committerGitHub <noreply@github.com>2020-11-19 11:30:52 -0800
commit0d949be444e52f42de4f920d71512c95ff96666d (patch)
treee0fb946c294eb4f1365ac8a890997c964bbfa28c /src/include
parentf172b30bfe18a24416fd61f4aa5ce3dea583296e (diff)
Include stddef.h (needed for size_t) in cvc4_public.h (#5476)
This further removes obsolete explicit includes of stdint.h.
Diffstat (limited to 'src/include')
-rw-r--r--src/include/cvc4_public.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h
index 85a41dfd3..0e43335db 100644
--- a/src/include/cvc4_public.h
+++ b/src/include/cvc4_public.h
@@ -19,6 +19,7 @@
#ifndef CVC4_PUBLIC_H
#define CVC4_PUBLIC_H
+#include <stddef.h>
#include <stdint.h>
#if defined _WIN32 || defined __CYGWIN__
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback