[sawfish] OPTIONS updated

[Christopher Bratusek <chrisb src gnome org>]

commit 84147ce50359b8d66c9eddb343c1a8cf97fbd8b3
Author: chrisb <zanghar freenet de>
Date:   Thu May 7 21:51:33 2009 +0200

    OPTIONS updated
---
 OPTIONS |    3 +++
 1 files changed, 3 insertions(+), 0 deletions(-)

diff --git a/OPTIONS b/OPTIONS
index 4fa8bd3..fd71eff 100644
--- a/OPTIONS
+++ b/OPTIONS
@@ -593,6 +593,9 @@
 ;; (define-special-variable tab-right-margin 16
 ;;   "Width of tab area's right-edge decoration")
 
+;; (define-special-variable tab-raise-on-hover nil
+;;   "Raise Tabs on Hover")    
+
 ;; shrink-yank options
 
 ;; (define-special-variable shrink-window-minimum-size 10