]> git.tue.mpg.de Git - adu.git/commitdiff
Merge branch 'master' into next next pu
authorAndre Noll <maan@tuebingen.mpg.de>
Fri, 3 May 2019 22:49:44 +0000 (00:49 +0200)
committerAndre Noll <maan@tuebingen.mpg.de>
Fri, 3 May 2019 22:49:44 +0000 (00:49 +0200)
* master:
  Remove some duplicate const specifiers.
  Add link to author homepage.
  Reword summary text.
  create: Make the directory scan more robust.


Trivial merge