diff options
| -rw-r--r-- | documentation/dev-manual/dev-manual-common-tasks.xml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/documentation/dev-manual/dev-manual-common-tasks.xml b/documentation/dev-manual/dev-manual-common-tasks.xml index fc276e51ee..0476c5a5f1 100644 --- a/documentation/dev-manual/dev-manual-common-tasks.xml +++ b/documentation/dev-manual/dev-manual-common-tasks.xml | |||
| @@ -10612,7 +10612,7 @@ | |||
| 10612 | mkdir -p $src_release_dir/$p/source | 10612 | mkdir -p $src_release_dir/$p/source |
| 10613 | cp $d/* $src_release_dir/$p/source 2> /dev/null | 10613 | cp $d/* $src_release_dir/$p/source 2> /dev/null |
| 10614 | mkdir -p $src_release_dir/$p/license | 10614 | mkdir -p $src_release_dir/$p/license |
| 10615 | cp tmp/deploy/licenses/$p/* source-release/$p/license 2> /dev/null | 10615 | cp tmp/deploy/licenses/$p/* $src_release_dir/$p/license 2> /dev/null |
| 10616 | fi | 10616 | fi |
| 10617 | done | 10617 | done |
| 10618 | done </literallayout> | 10618 | done </literallayout> |