Oops - that's the second time I made this mistake - I was unwittingly committing to a branch in the git repo. Try it again (I hope it's fixed now).
Perfect, works great! btw, in my case a make install inside bob~s source directory created a folder /usr/local/lib/pd/extra/bob~ that had no read nor execute permissions set for other (all) users. Is this expected and standard behavior?
Thanks, Peter