diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 22 |
1 files changed, 22 insertions, 0 deletions
@@ -588,6 +588,7 @@ qemu_targets enable_libsanitizer with_linux_headers_src with_pk_src +with_dejagnu_src with_spike_src with_qemu_src with_gdb_src @@ -699,6 +700,7 @@ with_gdb_src with_qemu_src with_spike_src with_pk_src +with_dejagnu_src with_linux_headers_src enable_libsanitizer enable_qemu_system @@ -3730,6 +3732,26 @@ fi } +{ + +# Check whether --with-dejagnu-src was given. +if test "${with_dejagnu_src+set}" = set; then : + withval=$with_dejagnu_src; +else + with_dejagnu_src=default + +fi + + if test "x$with_dejagnu_src" != xdefault; then : + with_dejagnu_src=$with_dejagnu_src + +else + with_dejagnu_src="\$(srcdir)/dejagnu" + +fi + + } + # Check whether --with-linux-headers-src was given. if test "${with_linux_headers_src+set}" = set; then : |