diff options
Diffstat (limited to 'gas/configure')
| -rwxr-xr-x | gas/configure | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/gas/configure b/gas/configure index 16a8937..e39c965 100755 --- a/gas/configure +++ b/gas/configure @@ -12609,7 +12609,7 @@ _ACEOF { $as_echo "$as_me:${as_lineno-$LINENO}: result: $with_isa_spec" >&5 $as_echo "$with_isa_spec" >&6; } - # --with-priv-spec=[1.9.1|1.10|1.11|1.12]. + # --with-priv-spec=[1.9.1|1.10|1.11|1.12|1.13]. { $as_echo "$as_me:${as_lineno-$LINENO}: checking for default configuration of --with-priv-spec" >&5 $as_echo_n "checking for default configuration of --with-priv-spec... " >&6; } if test "x${with_priv_spec}" != x; then |