- {
- if (spent_usec < 250000)
- {
- fprintf (stderr, "returned too early\n");
- exit (1);
- }
- /* Timeout */
- printf ("."); fflush (stdout);
- }
+ {
+ if (spent_usec < 250000)
+ {
+ fprintf (stderr, "returned too early\n");
+ exit (1);
+ }
+ /* Timeout */
+ printf (".");
+ ASSERT (fflush (stdout) == 0);
+ }