2,177 karma · joined December 20, 2011
Host github_as_pulp
Hostname github.com
User git
IdentityFile ~/.ssh/pulp.../id_rsa
IdentitiesOnly yes
I just need to replace github.com by github_as_pulp on my clone command to use my second github account. As it remains in .git/config, it matches automatically when I cd between repositories.In another script, I have GIT_SSH_COMMAND="ssh -i /.../.ssh/id_rsa -F /dev/null" git archive --remote=git@bor...fr:ace/docsite.git master | tar xp docsiteapp
git and ssh are so versatile. I think that a little documentation is better than a new tool.
Despite the apparent simplicity, you can develop very advanced game mechanism. The limitations occur when you want to give a professional finish. It is meant for children, but it is a pleasure also for the "parent teacher" because it allows to teach advanced ideas.
It is not a product. They open it so that public can contribute to help them.
They do not say the aim of this research.
The final user of the software will receive a changelog (a list of commit messages) that shall identify the bugs that have been fixed and the new user requirements that have been added. He needs to know why the code has changed to know what he has to do.
We can leave hands in water at 50°C. Above, it slightly start to cause burns.
This is a range that make a lot of sense IMHO.
At my work, I was present when the research on ASAS (https://skybrary.aero/articles/airborne-separation-assurance...) led to the idea of PMS (https://www.eurocontrol.int/sites/default/files/2021-05/euro...).
Never underestimate serendipity