A question came up about updates to code in the "users" area of hps-java....
Since this code is not tightly managed, changes do not need to have github issues. But a specific pull request is still needed. So developers can use a generic branch name like 'jeremy-dev' for merging these changes which would be approved basically upon
Otherwise the procedure is more or less the same as I outlined in the PR instructions.
Let me know if you have any questions.