8f36d86 Merge #66 `Put Kerberos options in rida config`

3 files Merged by mprahl 7 years ago, Committed by nphilipp 7 years ago,
    Merge #66 `Put Kerberos options in rida config`
    
        
file modified
+5 -0
file modified
+5 -7
file modified
+27 -0