diff --git a/842c4eda7f6b7244414f425504281e797ac877ef b/842c4eda7f6b7244414f425504281e797ac877ef new file mode 100644 index 000000000..fc17a7d09 --- /dev/null +++ b/842c4eda7f6b7244414f425504281e797ac877ef @@ -0,0 +1,7 @@ +Verified+1: Jenkins +Code-Review+2: Lionel Sambuc +Submitted-by: David van Moolenbroek +Submitted-at: Wed, 21 Aug 2013 01:19:18 +0200 +Reviewed-on: http://gerrit-minix.few.vu.nl/754 +Project: minix +Branch: refs/heads/master