Allows for correct compilation even if no GIT repository is configures. #23

Closed
wants to merge 1 commit into
from

Projects

None yet

2 participants

@shadinger
Contributor

Compilation would fail if not GIT repository is configured, because "buildInfos.ml" would contain :

(line 11)
let opalang_git_version =

instead of

let opalang_git_version = 0

@akoprow akoprow closed this Nov 24, 2011
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment