[ ] I have filed an issue about this change and discussed potential changes with the maintainers.
[X] I have received the approval from the maintainers to make this change.
[X] This is not a stylistic, refactoring, or cleanup change.
Please note that the maintainers will not be reviewing this change until all checkboxes are ticked. See
the Contributions section in the README for more
details.
Discussion thread for this change
Issue number: N/A
Description of this change
If a user has set workspace( name = "something") in their WORKSPACE file, we should probably default to that instead of the name the directory happens to have.
Checklist
Please note that the maintainers will not be reviewing this change until all checkboxes are ticked. See the Contributions section in the README for more details.
Discussion thread for this change
Issue number:
N/ADescription of this change
If a user has set
workspace( name = "something")in theirWORKSPACEfile, we should probably default to that instead of the name the directory happens to have.