Summary
.gitignore has "docs/" as a folder to ignore the files from. It should be "/docs/", else any docs subfolder is also ignored.

Motivation

• If the problem does occur, what are the consequences and how severe are they?
  I noticed this issue when I was adding new documentation, so a new file into "src/docs/" folder. The files were ignored because of .gitignore, and I had to to a fierce add "git add -f".

The issue is that if a '/' is not given at the start of the pattern, .gitignore matches the pattern to a subfolder too. Here is a blurb from the .gitignore documentation:

The slash / is used as the directory separator. Separators may occur at the beginning, middle or end of the .gitignore search pattern.

If there is a separator at the beginning or middle (or both) of the pattern, then the pattern is relative to the directory level of the particular .gitignore file itself. Otherwise the pattern may also match at any level below the .gitignore level.

• Is this issue urgent?
  No

Acceptance Criteria (Definition of Done) / Testing
Test that new files can be "git add" without force from "/src/docs/" folder.

• Documentation update
  None