From 06ea44c895a5f97b7b9b65fce84dec2700f443fb Mon Sep 17 00:00:00 2001
From: Ori Bernstein <ori@eigenstate.org>
Date: Tue, 10 Mar 2020 09:35:06 -0700
Subject: [PATCH] fix -T option for doctype

We used to set $dev to -T, and leave the device type
in the argument list. Now, we set it to -T$2, and shift
it out of the list.
---
 rc/bin/doctype | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/rc/bin/doctype b/rc/bin/doctype
index e027fe13b..0f04f91ef 100755
--- a/rc/bin/doctype
+++ b/rc/bin/doctype
@@ -13,7 +13,8 @@ while(~ $1 -*){
 		eqn=neqn
 		prefer='prefer -n'
 	case -T
-		dev=$1
+		dev=-T$2
+		shift
 	case -*
 		opt=$opt' $1'
 	}