[cave9] (4 commits) ...Git ignore file

[Victor Bogado da Silva Lins]

Summary of changes:

  b2556ca... Initialize branch F-13 for cave9 (*)
  3d0d1e3... dist-git conversion (*)
  d188b46... Merge branch 'master' into f13
  6318de4... Git ignore file

(*) This commit already existed in another branch; no separate mail sent