Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #1104 from protegeproject/dont-override-user-exten…
…sion Do not override user-provided extension.