Fix type error in benchmark.h

This commit is contained in:
Kent McLeod 2017-02-27 09:29:24 +11:00
parent aa656604db
commit 325db51cb1
2 changed files with 4 additions and 4 deletions

View file

@ -27,8 +27,8 @@
extern timestamp_t ksEntries[CONFIG_MAX_NUM_TRACE_POINTS];
extern bool_t ksStarted[CONFIG_MAX_NUM_TRACE_POINTS];
extern timestamp_t ksExit;
extern uint32_t ksLogIndex;
extern uint32_t ksLogIndexFinalized;
extern seL4_Word ksLogIndex;
extern seL4_Word ksLogIndexFinalized;
extern paddr_t ksUserLogBuffer;
static inline void

View file

@ -33,8 +33,8 @@ extern kernel_entry_t ksKernelEntry;
sizeof(benchmark_track_kernel_entry_t))
extern timestamp_t ksEnter;
extern word_t ksLogIndex;
extern uint32_t ksLogIndexFinalized;
extern seL4_Word ksLogIndex;
extern seL4_Word ksLogIndexFinalized;
/**
* @brief Fill in logging info for kernel entries