You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
(* (c) Syncgit - Lucas Baudin <[email protected]> – 2015 - see LICENSE file. *)
open Config_file
let conf = new group
let path_git_ = new string_cp ~group:conf ["path_git"] "/tmp/git" "Path where we can store the git repositories. It must exist with the appropriate permission."
let github_user_ = new string_cp ~group:conf ["github_user"] "hackens" "GitHub user"
let github_url_ = new string_cp ~group:conf ["github_url"] "[email protected]:" "GitHub URL"
let source_prefix_ = new string_cp ~group:conf ["source_prefix"] "https://git.eleves.ens.fr/hackens/" "Must be used for security reasons: otherwise, anyone get sync anything to your git repositories."