It's OK in the sense that it's not a security emergency, but, don't use HMAC-SHA1 (or HMAC-MD5, which is also in the same sense "ok").
If you do know the secret key, collisions are easy, but probably pointless since you can already forge HMAC signatures for anything you want.
Still, even if there’s no way to break HMAC-SHA1 (or even HMAC-MD5) faster than the birthday attack, you should still prefer to pick a better hash algorithm for safety.
In this specific case, it's unclear whether the bug has direct security implications. The broken SHA-1 is used on some user-controlled data that gets XORed onto the server's decryption of a user-specified payload before being passed into an RC4 key schedule. It's certainly plausible that this might produce a server-assisted privacy compromise of other users' sessions.