Mirek Kratochvil 91900a323c add a script for sourcing the timestamps from gits ... Fixes #2		2023-06-22 11:43:28 +02:00
..
make-search-index.js	make a separate scripts directory (this gonna grow)	2023-06-22 11:43:28 +02:00
source-timestamps.sh	add a script for sourcing the timestamps from gits	2023-06-22 11:43:28 +02:00