Draft: Add HTTOKENOPTS to bashrc
This was previously in the crontab, but I think it needs to be in the bashrc for it to take the right value at login. Related to #685 (closed).
This was previously in the crontab, but I think it needs to be in the bashrc for it to take the right value at login. Related to #685 (closed).