Geoffroy Van Cutsem ff91d07337 doc: update .gitignore to reflect the new location of the tools ...

Update the .gitignore file to reflect the fact that the tools are now located
under misc/ and no longer under tools/.

One of the temporary folder created during the documentation generation was
doc/tools and it was therefore ignored by Git. It is now better to *not*
ignore it as it will cause documention build issues if such previous folder
exists.

Signed-off-by: Geoffroy Van Cutsem <geoffroy.vancutsem@intel.com>

2019-09-10 12:13:58 +02:00

101 B

Raw Blame History

View Raw