From 75719826068cf7f699811155ba0e7ff93e61b326 Mon Sep 17 00:00:00 2001
From: George Beckstein <donbeckstein@live.com>
Date: Mon, 12 Oct 2020 12:05:38 -0400
Subject: [PATCH] Fix MBED_ERROR call in init_os_timer

---
 platform/source/mbed_os_timer.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/platform/source/mbed_os_timer.cpp b/platform/source/mbed_os_timer.cpp
index 9fcf1b1793..d7b2f075b1 100644
--- a/platform/source/mbed_os_timer.cpp
+++ b/platform/source/mbed_os_timer.cpp
@@ -52,7 +52,11 @@ OsTimer *init_os_timer()
 #elif DEVICE_USTICKER
         os_timer = new (os_timer_data) OsTimer(get_us_ticker_data());
 #else
-        MBED_ERROR("OS timer not available");
+        MBED_ERROR(
+            MBED_MAKE_ERROR(
+                MBED_MODULE_PLATFORM,
+                MBED_ERROR_CODE_CONFIG_UNSUPPORTED),
+            "OS timer not available");
 #endif
     }