On Fri, 1 Dec 2017 13:26:05 +0100 Sebastian Andrzej Siewior <bigeasy@xxxxxxxxxxxxx> wrote: > - disable RT_PUSH_IPI if booted on UP. After all there is not much > benefit here, is there? This is what I would suggest. Maybe I'll look at adding a patch. -- Steve -- To unsubscribe from this list: send the line "unsubscribe linux-rt-users" in the body of a message to majordomo@xxxxxxxxxxxxxxx More majordomo info at http://vger.kernel.org/majordomo-info.html
