1.1 --- a/docs/tools/profile_prefs.sh Thu Nov 05 20:00:51 2015 +0100
1.2 +++ b/docs/tools/profile_prefs.sh Fri Nov 06 00:00:55 2015 +0100
1.3 @@ -10,8 +10,8 @@
1.4 echo "|| '''Label''' || '''Setting''' ||"
1.5
1.6 grep '^ \+("' "$PROFILE" \
1.7 -| sed 's/^ \+("\(.*\)".*, \+"\(.*\)"),$/|| \2 || [[..\/Preferences#\1|\1]] ||/'
1.8 +| sed 's/^ \+("\(.*\)".*, \+_("\(.*\)")),$/|| \2 || [[..\/Preferences#\1|\1]] ||/'
1.9
1.10 # Convert from... to...
1.11 -# ("setting" , "label"),
1.12 +# ("setting" , _("label")),
1.13 # || label || [[../Preferences#setting|setting]] ||