Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Version dune-workspace and user config files #929

Closed
ghost opened this issue Jun 29, 2018 · 1 comment
Closed

Version dune-workspace and user config files #929

ghost opened this issue Jun 29, 2018 · 1 comment
Milestone

Comments

@ghost
Copy link

ghost commented Jun 29, 2018

The last files that are not versioned are dune-workspace files and the user configuration file in ~/.config/dune/config. It seems worth versioning them before the 1.0.0 otherwise it will be hard to do it afterwards. It is a bit more complicated to version those and keep backward compatibility, so I suggest the following plan:

  • jbuilder ignores dune-workspace files
  • jbuilder parses workspace files in jbuild syntax
  • jbuilder accepts a user configuration file without (lang ...) and in this case parses it in jbuild syntax
  • dune ignores jbuild-workspace and jbuild-workspaceXXX files
  • dune requires (lang dune ...) in workspace files
  • dune requires (lang dune ...) in the user configuration file
@ghost ghost added this to the 1.0.0 milestone Jun 29, 2018
@ghost ghost self-assigned this Jun 29, 2018
@ghost
Copy link
Author

ghost commented Jul 1, 2018

This is now done

@ghost ghost closed this as completed Jul 1, 2018
This issue was closed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

0 participants