From a1e598f1cb3f96af948aed762df7aafb661ab8f5 Mon Sep 17 00:00:00 2001 From: Hyacinthe Cartiaux Date: Thu, 6 Mar 2014 01:30:00 +0100 Subject: [PATCH] [wget,install] wgetrc configuration, specific config for g5k --- install.sh | 8 ++++++++ wget/wgetrc | 28 ++++++++++++++++++++++++++++ wget/wgetrc.g5k | 32 ++++++++++++++++++++++++++++++++ 3 files changed, 68 insertions(+) create mode 100644 wget/wgetrc create mode 100644 wget/wgetrc.g5k diff --git a/install.sh b/install.sh index ebb8989..1c1eb31 100755 --- a/install.sh +++ b/install.sh @@ -64,6 +64,14 @@ mkdir -p ~/.rtorrent ln -sf $DOTFILES/git/gitconfig ~/.gitconfig +## wget + +if [[ "`hostname -f | cut -d '.' -f 3`" = "grid5000" ]] ; then + ln -sf $DOTFILES/wget/wgetrc.g5k ~/.wgetrc +else + ln -sf $DOTFILES/wget/wgetrc ~/.wgetrc +fi + ## ssh mkdir -p ~/.ssh/sockets diff --git a/wget/wgetrc b/wget/wgetrc new file mode 100644 index 0000000..901f45d --- /dev/null +++ b/wget/wgetrc @@ -0,0 +1,28 @@ +################################################################################ +# .wgetrc -- configuration file for [wget](https://www.gnu.org/software/wget/) +# _ +# __ ____ _ ___| |_ _ __ ___ +# \ \ /\ / / _` |/ _ \ __| '__/ __| +# \ V V / (_| | __/ |_| | | (__ +# (_)_/\_/ \__, |\___|\__|_| \___| +# |___/ +# +################################################################################ +# +## You can use this file to change the default behaviour of wget or to +## avoid having to type many many command-line options. This file does +## not contain a comprehensive list of commands -- look at the manual +## to find out what you can put into this file. You can find this here: +## $ info wget.info 'Startup File' +## Or online here: +## https://www.gnu.org/software/wget/manual/wget.html#Startup-File +## +## Wget initialization file can reside in /usr/local/etc/wgetrc +## (global, for all users) or $HOME/.wgetrc (for a single user). + +# Use timestamping by default +timestamping = on + +# If set to on, use the last component of a redirection URL for the local file name. +continue = on + diff --git a/wget/wgetrc.g5k b/wget/wgetrc.g5k new file mode 100644 index 0000000..76d903d --- /dev/null +++ b/wget/wgetrc.g5k @@ -0,0 +1,32 @@ +################################################################################ +# .wgetrc -- configuration file for [wget](https://www.gnu.org/software/wget/) +# _ +# __ ____ _ ___| |_ _ __ ___ +# \ \ /\ / / _` |/ _ \ __| '__/ __| +# \ V V / (_| | __/ |_| | | (__ +# (_)_/\_/ \__, |\___|\__|_| \___| +# |___/ +# +################################################################################ +# +## You can use this file to change the default behaviour of wget or to +## avoid having to type many many command-line options. This file does +## not contain a comprehensive list of commands -- look at the manual +## to find out what you can put into this file. You can find this here: +## $ info wget.info 'Startup File' +## Or online here: +## https://www.gnu.org/software/wget/manual/wget.html#Startup-File +## +## Wget initialization file can reside in /usr/local/etc/wgetrc +## (global, for all users) or $HOME/.wgetrc (for a single user). + +# G5K proxy settings +http_proxy = http://proxy:3128 +use_proxy = on + +# Use timestamping by default +timestamping = on + +# If set to on, use the last component of a redirection URL for the local file name. +continue = on +