diff options
Diffstat (limited to 'includes/rts/LibdwPool.h')
| -rw-r--r-- | includes/rts/LibdwPool.h | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/includes/rts/LibdwPool.h b/includes/rts/LibdwPool.h new file mode 100644 index 0000000000..3360192725 --- /dev/null +++ b/includes/rts/LibdwPool.h @@ -0,0 +1,22 @@ +/* --------------------------------------------------------------------------- + * + * (c) The GHC Team, 2015-2016 + * + * A pool of libdw sessions + * + * --------------------------------------------------------------------------*/ + +#ifndef RTS_LIBDW_POOL_H +#define RTS_LIBDW_POOL_H + +/* Claim a session from the pool */ +LibdwSession *libdwPoolTake(void); + +/* Return a session to the pool */ +void libdwPoolRelease(LibdwSession *sess); + +/* Free any sessions in the pool forcing a reload of any loaded debug + * information */ +void libdwPoolClear(void); + +#endif /* RTS_LIBDW_POOL_H */ |