Get rid of files where we don't own the copyright or license is unclear

[zsh-lovers.git] / zsh_people / bruno_bonfils / rc / options.rc

diff --git a/zsh_people/bruno_bonfils/rc/options.rc b/zsh_people/bruno_bonfils/rc/options.rc
deleted file mode 100644 (file)
index 4af4c3d..0000000
--- a/zsh_people/bruno_bonfils/rc/options.rc
+++ /dev/null
@@ -1,18 +0,0 @@
-# -*- shell-script -*-
-#
-# Zsh Options
-#
-
-export LISTPROMPT      # in order to scroll if completion list is too big
-
-setopt auto_cd         # a commande like % /usr/local is equivalent to cd /usr/local
-setopt nohup            # don't send HUP signal when closing term session
-setopt extended_glob   # in order to use #, ~ and ^ for filename generation
-setopt always_to_end   # move to cursor to the end after completion
-setopt notify          # report the status of backgrounds jobs immediately
-setopt correct         # try to correct the spelling if possible
-setopt rmstarwait      # wait 10 seconds before querying for a rm which contains a *
-setopt printexitvalue   # show the exit-value if > 0
-
-# Don't ecrase file with >, use >| (overwrite) or >> (append) instead 
-set -C