# HG changeset patch
# User Richard M. Stallman <rms@gnu.org>
# Date 781261949 0
# Node ID 07d0aeb633d815aa9f891efde30833d071b38b57
# Parent  bbacb08f7e0c490cc7def6fa1992368ac92bc823
Translate -gnu/linux* to -linux*.

diff -r bbacb08f7e0c -r 07d0aeb633d8 config.sub
--- a/config.sub	Tue Oct 04 09:03:20 1994 +0000
+++ b/config.sub	Tue Oct 04 09:12:29 1994 +0000
@@ -565,6 +565,9 @@
 	-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.