changeset 9255:07d0aeb633d8

Translate -gnu/linux* to -linux*.
author Richard M. Stallman <rms@gnu.org>
date Tue, 04 Oct 1994 09:12:29 +0000
parents bbacb08f7e0c
children 50532339ab7a
files config.sub
diffstat 1 files changed, 3 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- 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.