[PATCHv3] BZ#13750: Do not build manual in the source directory

[Andreas Schwab]

Andreas Jaeger <aj@suse.com> writes:

> Btw. you might want to delete the generated files from your local source
>  directory now - run "git status" to see what's extra.
>
> I just run:

$ git clean -f manual

Andreas.

-- 
Andreas Schwab, schwab@linux-m68k.org
GPG Key fingerprint = 58CA 54C7 6D53 942B 1756  01D3 44D5 214B 8276 4ED5
"And now for something completely different."