RTX tickless idle documentation bug

The example for tickless idle documented here: https://www.keil.com/pack/doc/CMSIS/RTOS2/html/theory_of_operation.html#TickLess  is missing an important check.

If RTX doesn't actually need to wake back up "after some time", osKernelSuspend returns osWaitForever (0xFFFFFFFF).  In that case you should NOT use the RTC to wake the system up.  Instead letting other interrupts do that job.

The documented example is for MSP32, which is not my platform, but for STM32L4 it looks something like this:

__NO_RETURN void osRtxIdleThread (void *argument) 
{
   (void)argument;
   uint32_t expectedIdleTime;
   uint32_t actualIdleTime = 0;
   for (;;)
   {
      expectedIdleTime  = osKernelSuspend();
      if (expectedIdleTime  > 0) {
         // Enter the low power state
         actualIdleTime = 0;
         HAL_SuspendTick();
         // If the kernel needs to wake up "after some time", use the RTC to do that
         if (expectedIdleTime != osWaitForever) {
            HAL_RTCEx_SetWakeUpTimer_IT(&rtcHandle, expectedIdleTime<<1, RTC_WAKEUPCLOCK_RTCCLK_DIV16);
         }

         HAL_PWREx_EnterSTOP2Mode(PWR_STOPENTRY_WFI);
            
         if (expectedIdleTime != osWaitForever) {
            actualIdleTime = HAL_RTCEx_GetWakeUpTimer(&rtcHandle)>>1;
            HAL_RTCEx_DeactivateWakeUpTimer(&rtcHandle);
            expectedIdleTime = actualIdleTime;
         }
         HAL_ResumeTick();    
      }
      // Adjust the kernel ticks with the amount of ticks slept
      osKernelResume (expectedIdleTime);
   }
}

void RTC_WKUP_IRQHandler(void)
{
   HAL_RTCEx_WakeUpTimerIRQHandler(&rtcHandle);
}