+{
+ /* Spin (with pre-emption enabled) waiting for console_ring_try_empty()
+ * to complete output. There is a small window here where we could
+ * end up with a stale value of console_output, but it's unlikely,
+ * and _cnputc(), which outputs to the console device, is internally
+ * synchronized. There's something of a conflict between the
+ * character-at-a-time (with pre-emption enabled) unbuffered
+ * output model here, and the buffered output from cnputc(),
+ * whose consumers include printf() ( which outputs a sequence
+ * with pre-emption disabled, and should be safe to call with
+ * interrupts off); we don't want to disable pre-emption indefinitely
+ * here, and spinlocks and mutexes are inappropriate.
+ */
+ while (console_output != 0);
+