Fix help lint for user-id

2010-02-05 01:20:40 -06:00 · 2010-02-05 01:20:40 -06:00 · 7d73d85856
parent f72bcd3346
commit 7d73d85856
1 changed files with 1 additions and 1 deletions
--- a/basis/unix/users/users-docs.factor
+++ b/basis/unix/users/users-docs.factor
@ -62,7 +62,7 @@ HELP: user-name
 HELP: user-id
 { $values
     { "string" string }
-     { "id" integer } }
+     { "id/f" "an integer or f" } }
 { $description "Returns the user id associated with the user-name." } ;

 HELP: with-effective-user