From 325db51cb108cd16af6aaa353d59c72807563fe6 Mon Sep 17 00:00:00 2001
From: Kent McLeod <Kent.Mcleod@data61.csiro.au>
Date: Mon, 27 Feb 2017 09:29:24 +1100
Subject: [PATCH] Fix type error in benchmark.h

---
 include/benchmark/benchmark.h       | 4 ++--
 include/benchmark/benchmark_track.h | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/include/benchmark/benchmark.h b/include/benchmark/benchmark.h
index 7db9f84c6..91d57d602 100644
--- a/include/benchmark/benchmark.h
+++ b/include/benchmark/benchmark.h
@@ -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
diff --git a/include/benchmark/benchmark_track.h b/include/benchmark/benchmark_track.h
index ff10edd06..1dbc125a3 100644
--- a/include/benchmark/benchmark_track.h
+++ b/include/benchmark/benchmark_track.h
@@ -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