[12:59:13] hello! How long does it typically take for a newly-created Toolforge tool to become become-able? I created https://toolhub.wikimedia.org/tools/tlepage-playground around 40 minutes ago and ssh login.toolforge.org become tlepage-playground keeps saying "become: no such tool 'tlepage-playground'" [13:00:28] interestingly I don’t see it listed in toolsadmin [13:11:55] thilp: hi! I'm not sure how long it is meant to be taking off the top of my head, I remember having a similar problem with 'cloudvps-quota' tool and after "a while" it worked, maybe an hour or so ? [13:15:29] thanks! I ended up creating it in toolsadmin too, and since then it took less than 10 minutes. I’ll follow-up to understand what happened via toolhub [13:15:58] *nod* sounds like a plan [13:27:13] thilp: toolhub is a discovery catalog. it does not impact the actual existence of resources on other systems [13:30:34] is its catalog regularly merged or overwritten with the actual tools from https://toolsadmin.wikimedia.org/tools/? or tool maintainers update both catalogs independently? [13:45:37] the tool info records managed via toolsadmin are one of many toolhub's data sources [14:29:53] interesting, I had no idea! do you know where I can read more about these other data sources? [15:23:20] thilp: https://toolhub.wikimedia.org/crawler-history [15:25:33] thilp: My question for you is what docs or UI features led you to believe that making a toolinfo record in Toolhub would be the way to create a new Toolforge tool? I know naming is hard and things are messy, so fixing extra confusing docs is a thing I like to do. [15:29:57] bd808: what's the best way to report spam like https://toolhub.wikimedia.org/tools/aynure [15:31:31] RhinosF1: I guess by poking me :/ That one is gone now. [15:32:58] bd808: thanks :) [15:34:22] RhinosF1: Do you want a new hat? I have the super powers to give out hats in Toolhub that would let you patrol things. [15:34:59] bd808: sure [15:38:49] RhinosF1: I added you to the patroller and oversighters groups -- https://meta.wikimedia.org/wiki/Toolhub#User_permission_levels [15:39:08] I think you have to have admin to delete... I need to check that. [15:41:15] I can't see a delete button [15:41:53] yeah, not button. Deletes can be done with the API browser at https://toolhub.wikimedia.org/api-docs#delete-/api/tools/-name-/ [15:44:35] RhinosF1: here, another hat: 🎩 [15:46:03] (Just sayin' mine is /much/ more fashionable than bd808's.) [15:49:47] bd808: that works [15:49:54] perryprog: heh :) [16:19:15] RhinosF1: I went digging in the Toolhub source code to try and remind myself how the permissions system works. The delete action for a toolinfo record right now requires that either you are the creator of the record or in the admin group. https://gerrit.wikimedia.org/r/plugins/gitiles/wikimedia/toolhub/+/refs/heads/main/toolhub/permissions.py#206 [16:23:56] RhinosF1: so... you are an admin now. Congratulations. Let me know how things go. [16:25:39] Thanks :)