diff options
| author | Xi Ruoyao <xry111@mengyan1223.wang> | 2021-07-06 23:00:16 +0800 |
|---|---|---|
| committer | Xi Ruoyao <xry111@mengyan1223.wang> | 2021-07-06 23:00:16 +0800 |
| commit | b1fb9310035ea0414edc2fa6c7493d371d787b7a (patch) | |
| tree | a41f7e6197a371edd3e65e30e589c678aa0cd182 /chapter08 | |
| parent | 3e8234557c4e07a85c578b8a993dce3365754df5 (diff) | |
DejaGNU: build in seperate directory
Upstream recommends it. And there are reports about test failure when
DejaGNU is build in source directory ("./configure").
Diffstat (limited to 'chapter08')
| -rw-r--r-- | chapter08/dejagnu.xml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/chapter08/dejagnu.xml b/chapter08/dejagnu.xml index da6a44aa9..169ad4b50 100644 --- a/chapter08/dejagnu.xml +++ b/chapter08/dejagnu.xml @@ -42,11 +42,17 @@ <sect2 role="installation"> <title>Installation of DejaGNU</title> + <para>The upstream recommends building DejaGNU in a dedicated build + directory:</para> + +<screen><userinput remap="pre">mkdir -v build +cd build</userinput></screen> + <para>Prepare DejaGNU for compilation:</para> -<screen><userinput remap="configure">./configure --prefix=/usr -makeinfo --html --no-split -o doc/dejagnu.html doc/dejagnu.texi -makeinfo --plaintext -o doc/dejagnu.txt doc/dejagnu.texi</userinput></screen> +<screen><userinput remap="configure">../configure --prefix=/usr +makeinfo --html --no-split -o doc/dejagnu.html ../doc/dejagnu.texi +makeinfo --plaintext -o doc/dejagnu.txt ../doc/dejagnu.texi</userinput></screen> <para>Build and install the package:</para> |