Missing argument for macro SWITCH_CONTEXT

[KamelHacene]

File os/tpl_os_task_kernel.h, line 87 :

83      if (TPL_KERN(proc_core_id).need_schedule)
84     {
85       tpl_schedule_from_running(CORE_ID_OR_NOTHING(proc_core_id));
86       DOW_DO(printf("*S* ActivateTask - rescheduling done\n"));
87       SWITCH_CONTEXT(CORE_ID_OR_NOTHING(proc_core_id))
88      }

The macro SWITCH_CONTEXT (defined in os/tpl_os_kernel.h) takes one parameter.
Thus an error may be produced by the compiler (except gcc which does support that case) when CORE_ID_OR_NOTHING returns void.