After I helped him (it was a typo in a config file) I told him something I only learned half a year ago but I think is pretty handy. You can actually timestamp the commands in the history file.
The magical line is :
echo 'export HISTTIMEFORMAT="%d/%m/%y %T "' >> ~/.bash_profile
I also put it in my Dockerfile with the following instruction:
ENV HISTTIMEFORMAT="%d/%m/%y %T "