Merge pull request #768 from wenzhengjiang/remove_ppa_source
authordavid22swan <david.swan@puppet.com>
Thu, 23 Aug 2018 15:57:56 +0000 (16:57 +0100)
committerGitHub <noreply@github.com>
Thu, 23 Aug 2018 15:57:56 +0000 (16:57 +0100)
Make sure PPA source file is absent when apt-add-repository fails


Trivial merge