From 1a192c1543c5e67ba163f2551b9864635a8b255c Mon Sep 17 00:00:00 2001
From: Remzi Arpaci-Dusseau <remzi.arpacidusseau@gmail.com>
Date: Sun, 31 Mar 2019 08:49:14 -0500
Subject: [PATCH] need this script to auto-edit the xv6 Makefile for testing

---
 tester/xv6-edit-makefile.sh | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100755 tester/xv6-edit-makefile.sh

diff --git a/tester/xv6-edit-makefile.sh b/tester/xv6-edit-makefile.sh
new file mode 100755
index 000000000..c241209ca
--- /dev/null
+++ b/tester/xv6-edit-makefile.sh
@@ -0,0 +1,16 @@
+#! /bin/bash
+
+infile=$1
+testnames=$2
+
+gawk -vtestnames=$testnames '
+($1 == "_mkdir\\") {
+  n = split(testnames, x, ",");
+  for (i = 1; i <= n; i++) {
+    printf("\t_%s\\\n", x[i]);
+  }
+} 
+
+{
+  print $0;
+}' $infile