diff --git a/aaafe4b435456ad648cb3e57ab2e03528a89d2a2 b/aaafe4b435456ad648cb3e57ab2e03528a89d2a2 new file mode 100644 index 000000000..acb6d615b --- /dev/null +++ b/aaafe4b435456ad648cb3e57ab2e03528a89d2a2 @@ -0,0 +1,7 @@ +Verified+1: Jenkins +Code-Review+2: Ben Gras +Submitted-by: Thomas Cort +Submitted-at: Tue, 14 Jan 2014 11:53:13 +0100 +Reviewed-on: http://gerrit-minix.few.vu.nl/1205 +Project: minix +Branch: refs/heads/master