diff --git a/documentation/dev-manual/dev-manual-common-tasks.xml b/documentation/dev-manual/dev-manual-common-tasks.xml index 658919dfc0..2319be1d84 100644 --- a/documentation/dev-manual/dev-manual-common-tasks.xml +++ b/documentation/dev-manual/dev-manual-common-tasks.xml @@ -1885,8 +1885,11 @@ The previous example also specifies a patch file. - Patch files are files whose names end in - .patch or .diff. + Patch files are files whose names usually end in + .patch or .diff but + can end with compressed suffixes such as + diff.gz and + patch.bz2, for example. The build system automatically applies patches as described in the "Patching Code" section.