diff options
author | Karl Berry <karl@freefriends.org> | 2007-09-03 17:03:11 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2007-09-03 17:03:11 +0000 |
commit | 46b53cefa53aa754e0cc6c6f1095de5c7b2ffa34 (patch) | |
tree | a281fbde926b8f7bab11e1b6ee3c7a5260aff3a2 | |
parent | d4d1a38de7842f8d66c0e60fa6a702fd2deed84c (diff) |
default to /usr/share/info and /usr/share/man
(daniel mader 15 Jun 2007 11:56:03)
git-svn-id: svn://tug.org/texlive/trunk@4862 c570f23f-e606-0410-a88d-b1316a301751
-rwxr-xr-x | Master/common.sh | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/Master/common.sh b/Master/common.sh index 2815e1bffcf..850276fe744 100755 --- a/Master/common.sh +++ b/Master/common.sh @@ -758,14 +758,29 @@ menu_options() L) toggle opt_symlinks if test "$opt_symlinks" = X; then cls; textvar_show screen_3; echo + # opt_symlinks_bin=$opt_symlinks_bin_last test -z "$opt_symlinks_bin" && opt_symlinks_bin=/usr/bin gets opt_symlinks_bin 'binary directory' + # opt_symlinks_man=$opt_symlinks_man_last - test -z "$opt_symlinks_man" && opt_symlinks_man=`dirname $opt_symlinks_bin`/man + if test -z "$opt_symlinks_man"; then + if test "$opt_symlinks_bin" = /usr/bin; then + opt_symlinks_man=/usr/share/man # /usr/man no longer common + else + opt_symlinks_man=`dirname $opt_symlinks_bin`/man + fi + fi gets opt_symlinks_man 'man directory ' + # opt_symlinks_info=$opt_symlinks_info_last - test -z "$opt_symlinks_info" && opt_symlinks_info=`dirname $opt_symlinks_bin`/info + if test -z "$opt_symlinks_info"; then + if test "$opt_symlinks_bin" = /usr/bin; then + opt_symlinks_info=/usr/share/info # ditto for info + else + opt_symlinks_info=`dirname $opt_symlinks_bin`/info + fi + fi gets opt_symlinks_info 'info directory ' else opt_symlinks_bin_last=$opt_symlinks_bin |