|Mini tool to look up some basic infos on servers/hostnames|
|mario authored 149 days ago last checkin 8d7d5133e ⎘|
|📄 reddit.url||Derived from current base version 0.8.0; some sample and generic scri‹›||151 days ago|
The UserTools/ directory is used by tools/plugins/menu_userscripts.ps1
It's just an in-menu file copy function mostly.