build: maintainer-clean: Kill web_sync remove command.
authorAndre Noll <maan@tuebingen.mpg.de>
Mon, 7 Sep 2015 22:39:40 +0000 (00:39 +0200)
committerAndre Noll <maan@tuebingen.mpg.de>
Sun, 20 Sep 2015 18:32:53 +0000 (20:32 +0200)
commit6a22b3923f75436aaf84135bd397ab82f22bc09f
tree5c673e8f19bacd3a8b60f572ddb88d7c81638647
parentad0a32acc373428d38e6b0f2f244ac3c31eea7c5
build: maintainer-clean: Kill web_sync remove command.

This directory was used by a private script, but these days the script
creates its temporary files elsewhere. Hence it is no longer neccessary
to remove the directory in the receipe of the maintainer-clean target.
Makefile.real