When to push the commits

[F0urchette]

Description

As a teacher
I want the students' work to be regularly pushed
So that I can see their progress over the session
But we need to find the best time to push the commits as pushing all commits one by one is not relevant

Hints

Two options that are complementary :

• when the student closes a question (see Use a command to move on to the next question #2) : needed to have several progress points over a session
• when the student ends the script : needed to be sure at least one push is done

The last point will need investigation to be sure we can have a hook called when the script is about to end.

[F0urchette]

Also : set a timer (5 minutes, to be specified in a conf file) to push.