Index: /trunk/FACT++/src/Readline.cc
===================================================================
--- /trunk/FACT++/src/Readline.cc	(revision 10274)
+++ /trunk/FACT++/src/Readline.cc	(revision 10275)
@@ -470,6 +470,5 @@
 //
 //! Adds the given string to the history buffer of readline's history by
-//! calling add_history. If skip is set to true str will be compared
-//! with the last line added to the history and only be added if it difers.
+//! calling add_history. 
 //!
 //! @param str
@@ -478,10 +477,12 @@
 //!
 //! @param skip
-//!    If skip is true do not add a new entry if it is identical to
-//!    the last one.
-//
-void Readline::AddToHistory(const string &str, bool skip)
-{
-    if (skip && fLastLine==str)
+//!    If skip is 1 and str matches the last added entry in the history,
+//!    the entry is skipped. If skip==2, all entries matching str are
+//!    removed from the history before the new entry is added as last one.
+//!    <skip==2 is the default>
+//
+void Readline::AddToHistory(const string &str, int skip)
+{
+    if (skip==1 && fLastLine==str)
         return;
 
@@ -489,8 +490,22 @@
         return;
 
+    while (skip==2)
+    {
+        int p = history_search_pos(str.c_str(), 0, 0);
+        if (p<0)
+            break;
+
+        delete remove_history(p);
+    }
+
     add_history(str.c_str());
     fLastLine = str;
 }
 
+// --------------------------------------------------------------------------
+//
+//! @returns
+//!     a string containing [{fLine}]
+//
 string Readline::GetLinePrompt() const
 {
Index: /trunk/FACT++/src/Readline.h
===================================================================
--- /trunk/FACT++/src/Readline.h	(revision 10274)
+++ /trunk/FACT++/src/Readline.h	(revision 10275)
@@ -71,5 +71,5 @@
     std::string GetName() const { return fName; }
 
-    void AddToHistory(const std::string &str, bool skip=true);
+    void AddToHistory(const std::string &str, int skip=2);
     static bool ClearHistory();
     std::vector<const char*> GetHistory() const;
