]> https://gitweb.dealii.org/ - dealii.git/commit
Merge pull request #6953 from masterleinad/ignore_deleted
authorWolfgang Bangerth <bangerth@colostate.edu>
Sun, 22 Jul 2018 16:50:51 +0000 (10:50 -0600)
committerGitHub <noreply@github.com>
Sun, 22 Jul 2018 16:50:51 +0000 (10:50 -0600)
commit3b4258196e860c5c260a3a532b7bd2697cae95d9
tree3b446f71b9efe98c87c4c1f49d2128c23c70d9f5
parentabab6fd3ff2f461f9cdae7a41f0fa1fc9c1f63de
parent5ec43446818fbf7e4eb7f34735cf12bc0611495c
Merge pull request #6953 from masterleinad/ignore_deleted

Ignore deleted files when formatting

In the beginning the Universe was created. This has made a lot of people very angry and has been widely regarded as a bad move.

Douglas Adams


Typeset in Trocchi and Trocchi Bold Sans Serif.