From 19bb6f08769e62eec4350df3a0427099cbc8c792 Mon Sep 17 00:00:00 2001 From: Arnaud Giersch Date: Thu, 21 Mar 2013 15:08:23 +0100 Subject: [PATCH] Dumb commit: kill empty line. --- src/mc/mc_dpor.c | 1 - 1 file changed, 1 deletion(-) diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index 2e9cc17079..a97440a01d 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -255,7 +255,6 @@ void MC_dpor(void) xbt_fifo_item_t item = NULL; int pos; int visited_state; - while (xbt_fifo_size(mc_stack_safety) > 0) { -- 2.20.1