1 files changed, 8 insertions, 0 deletions
diff --git a/platforms/timer.c b/platforms/timer.c
new file mode 100644
index 0000000000..26038dcda3
--- /dev/null
+++ b/platforms/timer.c
@@ -0,0 +1,8 @@
+// Copyright 2023 Sergey Vlasov (@sigprof)
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+#include "timer.h"
+
+// Generate out-of-line copies for inline functions defined in timer.h.
+extern inline fast_timer_t timer_read_fast(void);
+extern inline fast_timer_t timer_elapsed_fast(fast_timer_t last);