git subrepo clone git@gitlab-ssh.irstea.fr:pole-is/devtools-config.git devtools

subrepo:
  subdir:   "devtools"
  merged:   "0c931beb"
upstream:
  origin:   "git@gitlab-ssh.irstea.fr:pole-is/devtools-config.git"
  branch:   "master"
  commit:   "0c931beb"
git-subrepo:
  version:  "0.3.1"
  origin:   "https://github.com/ingydotnet/git-subrepo"
  commit:   "a7ee886"