Hi all, hopefully someone here will be familiar with this. We're trying to make my user account on our local galaxy installation an administrator. We've added the associated email address to the
admin_users = other's, email, addresses, email@example.com) line in
config/galaxy.ini and restarted the server, but that doesn't seem to have had any effect (namely, I still don't see the "Admin" option when I log into galaxy). One complication is that galaxy is running within docker. I have read through How config the admin menu (adding an administrator in galaxy / biolinux) and, since at least the base server is running CentOS rather than Biolinux, the galaxy-add-administrator command doesn't seem to be present.
Is there a log file somewhere that I might look to help diagnose the cause of this or would someone else happen to know where we're going amiss? I do have root permissions on the server, though I would prefer to minimally mess with the server, since it's in use (though it's a 4 day weekend here, so there are no jobs currently running).
Edit: If it's useful, my account is currently the 4th of 4 accounts listed on the admin_users line. Is there perhaps some sort of hard limit to the accounts stored when the file is parsed (this would seem unlikely, but I figured I'd ask)?