From 571a8899fd67ce21968b0ba7c4b38f357fb55787 Mon Sep 17 00:00:00 2001 From: mattias Date: Sat, 23 Jun 2012 16:31:38 +0000 Subject: [PATCH] deb+rpm: default environmentoptions: updated to 107, removed default gdb entry git-svn-id: trunk@37745 - --- tools/install/linux/environmentoptions.xml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/tools/install/linux/environmentoptions.xml b/tools/install/linux/environmentoptions.xml index 152a690000..1174b2ded4 100644 --- a/tools/install/linux/environmentoptions.xml +++ b/tools/install/linux/environmentoptions.xml @@ -1,10 +1,7 @@ - - - - +