Make timeouts based on CPU time.

[pintos-anon] / src / utils / Makefile

diff --git a/src/utils/Makefile b/src/utils/Makefile
new file mode 100644 (file)
index 0000000..9eca3ba
--- /dev/null
+++ b/src/utils/Makefile
@@ -0,0 +1,7 @@
+all: setitimer-helper
+
+LDFLAGS = -lm
+setitimer-helper: setitimer-helper.o
+
+clean: 
+       rm -f *.o setitimer-helper