#! /bin/bash 
# Last edited on 2024-03-30 10:47:09 by stolfi
date '+%Y-%m-%d-%H%M%S'