Bigger history is nicer for ^R

diff --git a/.bash_profile b/.bash_profile
index 9a55cdccd311b4cc545150a86a979358f451800a..83660f7c3fba34173efebb944687ebc9705c9702 100644 (file)
--- a/.bash_profile
+++ b/.bash_profile
@@ -19,6 +19,7 @@ export CVS_RSH="ssh"
 export RSYNC_RSH="ssh"
 export PYTHONSTARTUP="$HOME/.pythonrc.py"
 export HISTCONTROL="ignoredups"
+export HISTSIZE="10000"
 
 # Local customisations
 [ -f ~/.bash_profile_local ] && source ~/.bash_profile_local