search

illinois-cs241 / broadway-on-demand

Webapp that facilitates on-demand assignment autograding via Broadway.
Other
11 stars 4 forks source link

Case-sensitive to github username #76

Closed zhengyao-lin closed 3 years ago

zhengyao-lin commented 5 years ago

One student from piazza has a capital letter in her github username(Ritchie5 vs. ritchie5). we should probably take the lower case before inserting usernames into db.

Although I'm not sure what the implication would be. Github is case-sensitive to usernames. Would it be possible for someone to fake other users with a different capitalization?

ayushr2 commented 5 years ago

If GitHub is case-sensitive to usernames, then we should not be lower casing usernames before adding to DB as it has the scope of breaking things (by using the wrong user).

Any reason you wanted to lower case the username before inserting in DB?

ayushr2 commented 4 years ago

@rod-lin bump?

PradyumnaShome commented 4 years ago

I think we are currently using the NetID as the repository name - we may have to separate those two purposes / store a mapping if they are different?

Xiangmingchen commented 4 years ago

Github user name is case-insensitive. Even though GHE returned a capitalized user name, we can still submit request to it with lower cased names and it will be applied to the same user.