Add "-k" option to pintos script. When used, pintos will scan the

[pintos-anon] / src / tests / filesys / extended / Make.tests

diff --git a/src/tests/filesys/extended/Make.tests b/src/tests/filesys/extended/Make.tests
index 1aeb8dd1acb68ba0071d6580b1b38f3d88662fd1..2ba4d76e5d1e2a5005512e45bc67518f2283bc93 100644 (file)
--- a/src/tests/filesys/extended/Make.tests
+++ b/src/tests/filesys/extended/Make.tests
@@ -27,7 +27,7 @@ tests/filesys/extended/syn-rw_PUTFILES += tests/filesys/extended/child-syn-rw
 
 GETTIMEOUT = 60
 
-GETCMD = pintos -v -T $(GETTIMEOUT)
+GETCMD = pintos -v -k -T $(GETTIMEOUT)
 GETCMD += $(PINTOSOPTS)
 GETCMD += $(SIMULATOR)
 GETCMD += --fs-disk=$(FSDISK)