diff options
| author | Tim King <taking@google.com> | 2016-02-01 11:28:33 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2016-02-01 11:28:33 -0800 |
| commit | 5b9cbe12ca8a9c0058e7bdf993b74fc45f1300d2 (patch) | |
| tree | b37ed200647a9af8f6b492fc9b83d83eaf25d04d /src | |
| parent | 52685068705546798b0a4d8204b10b848213975a (diff) | |
Generalizing the implementation of lib/clock_gettime.c so that it can always be compiled.
Diffstat (limited to 'src')
| -rw-r--r-- | src/lib/clock_gettime.c | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/src/lib/clock_gettime.c b/src/lib/clock_gettime.c index 01426dc51..3f1d36f0f 100644 --- a/src/lib/clock_gettime.c +++ b/src/lib/clock_gettime.c @@ -16,7 +16,7 @@ ** OS X). **/ -#warning "TODO: make lib/clock_gettime.h cvc4_private.h again." +#warning "TODO(taking): Make lib/clock_gettime.h cvc4_private.h again." #include "lib/clock_gettime.h" @@ -24,10 +24,6 @@ extern "C" { #endif /* __cplusplus */ -#if !(defined(__APPLE__) || defined(__WIN32__)) -# warning "This code assumes you're on Mac OS X or Win32, and you don't seem to be. You'll likely have problems." -#endif /* !(__APPLE__ || __WIN32__) */ - #ifdef __APPLE__ #include <stdio.h> @@ -64,7 +60,8 @@ long clock_gettime(clockid_t which_clock, struct timespec* tp) { return 0; } -#else /* else we're __WIN32__ */ +#else /* not defined __APPLE__ */ +#ifdef __WIN32__ #include <time.h> #include <windows.h> @@ -80,7 +77,8 @@ long clock_gettime(clockid_t which_clock, struct timespec* tp) { return 0; } -#endif /* __APPLE__ / __WIN32__ */ +#endif /* closing #ifdef __WIN32__ */ +#endif /* closing #else for #ifdef __APPLE__ / __WIN32__ */ #ifdef __cplusplus }/* extern "C" */ |