[ooo-build] [PATCH] do not patch extensions sources if they are disabled

[Jonathan Nieder]

Petr Mladek wrote:

> To be more precise. We need to split the diffs into two:
> 
> redirect-extensions.diff
> redirect-extensions-reportbuilder.diff
> 
> The second diff should be mentioned in the section [ ExtensionFixes ] in
> the ooo-build/patches/dev300/apply file.

Ok, ok. :)

Untested (will try when the current build finishes or tomorrow,
whichever comes first).