From 173dbcf7fedf037031e5ccdcdaab66394d233310 Mon Sep 17 00:00:00 2001
From: rms <rms>
Date: Tue, 4 Oct 1994 09:12:29 +0000
Subject: [PATCH] Translate -gnu/linux* to -linux*.

---
 config.sub | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/config.sub b/config.sub
index 61bd8d5..3893f4f 100755
--- a/config.sub
+++ b/config.sub
@@ -565,6 +565,9 @@ case $os in
 	-solaris)
 		os=-solaris2
 		;;
+	-gnu/linux*)
+		os=`echo $os | sed -e 's|gnu/linux|linux|'`
+		;;
 	# First accept the basic system types.
 	# The portable systems comes first.
 	# Each alternative must end in a *, to match a version number.