[rules-dev] Github is loosing changes of commits: only use the command line for now