revert #1124 (#1180)

problem in the definition of Tool.Indexing.dbpath: "~" in "~/.LPSearch.db" is not interpreted as the HOME directory
we revert #1124 by calling getenv HOME again
in case getenv HOME fails, we use ".LPSearch.db"

doc/options.rst

@@ -40,7 +40,7 @@ immediately stops on the first failure, without going to the next file
 
 **Remark on index:**
 
-The ``index`` command generates the file ``~/.LPSearch.db``. This file contains an indexation of all the symbols and rules occurring in the dk/lp files given in argument. By default, the file ``~/.LPSearch.db`` is erased first. To append new symbols and rules, use the option ``--add``. It is also possile to normalize terms wrt some rules before indexation by using ``--rules`` options.
+The ``index`` command generates the file ``~/.LPSearch.db`` if ``$HOME`` is defined, and ``.LPSearch.db`` otherwise. This file contains an indexation of all the symbols and rules occurring in the dk/lp files given in argument. By default, the db file is erased first. To append new symbols and rules, use the option ``--add``. It is also possile to normalize terms wrt some rules before indexation by using ``--rules`` options.
 
 **Remark on search:**
 

src/tool/indexing.ml

@@ -308,7 +308,10 @@ module DB = struct
 
  (* disk persistence *)
 
- let dbpath = "~/.LPSearch.db"
+ let dbpath =
+   match Sys.getenv_opt "HOME" with
+   | Some s -> s ^ "/.LPSearch.db"
+   | None -> ".LPSearch.db"
  let rwpaths = ref []
 
  let restore_from_disk () =