X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Foutput%2Fdriver.c;h=acc58cf999cdd7b77d533f54edc9ce17db954550;hb=127e4edd2968a7a566201ab7052976bb29b1182c;hp=5c5c8648864fd0866ed1312b405c803f68294497;hpb=32ee0e0402d6d56674f53a47d879ec5c07dabe09;p=pspp

diff --git a/src/output/driver.c b/src/output/driver.c
index 5c5c864886..acc58cf999 100644
--- a/src/output/driver.c
+++ b/src/output/driver.c
@@ -315,9 +315,8 @@ output_driver_create (struct string_map *options)
     device_type = SETTINGS_DEVICE_LISTING;
   else
     {
-      /* TRANSLATORS: Don't translate the words `terminal' or `listing'. */
-      error (0, 0, _("%s is not a valid device type (the choices are "
-                     "`terminal' and `listing')"), device_string);
+      error (0, 0, _("%s is not a valid device type (the choices are `%s' and `%s')"),
+                     device_string, "terminal", "listing");
       device_type = default_device_type (file_name);
     }