Thank you for this. I confess that part of me has a soft spot for the
original shell script implementation but if Python is faster and
indeed more portable then it makes sense to switch. I'll pull and
update as necessary.
Michael
On Fri, Nov 13, 2009 at 1:24 AM, Ondrej Certik ond...@certik.cz
Hello,
Make sure to rename the '_sources' directory in the searchtool.js,
line 389, or else the search page will not work correctly (I think
this directory name is hardcoded). In the python script, this is 'if
file.endswith(.html) or file.endswith(.js)', in bash this is 'find
-type f' without
Also, I read searchtool.js, it is a super cool gem. Very smart !
Cheers,
On Fri, Nov 13, 2009 at 3:01 PM, Jean Daniel
jeandaniel.bro...@gmail.com wrote:
Hello,
Make sure to rename the '_sources' directory in the searchtool.js,
line 389, or else the search page will not work correctly
On Fri, Nov 13, 2009 at 6:01 AM, Jean Daniel
jeandaniel.bro...@gmail.com wrote:
Hello,
Make sure to rename the '_sources' directory in the searchtool.js,
line 389, or else the search page will not work correctly (I think
this directory name is hardcoded). In the python script, this is 'if
