X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Fdevices%2Ftimer.c;h=befaaaed5a9a1ac0cd25ab76f8afd96fe6865127;hb=2e7e4557b7f84a1377d38c1b4db544251bcec317;hp=c97667f56bfcd5d9bd70862c7ff3ca2047f8f706;hpb=0214600879e9c25671857c1a33e7b79f7c2aa498;p=pintos-anon

diff --git a/src/devices/timer.c b/src/devices/timer.c
index c97667f..befaaae 100644
--- a/src/devices/timer.c
+++ b/src/devices/timer.c
@@ -73,7 +73,6 @@ timer_ticks (void)
   enum intr_level old_level = intr_disable ();
   int64_t t = ticks;
   intr_set_level (old_level);
-  barrier ();
   return t;
 }