Re: project.el: git submodules?

[Stefan Monnier]

>>> I even have a patch, but here's another thought: wouldn't this mistakenly
>>> punish people who keep their $HOME as a Git repository to sync
>>> between machines?
>> Depends if the Git worktrees within their $HOME use the same repository
>> as the one used for $HOME.
> Not 'git worktrees' (to be clear), just random other work directories, for
> work/hobby/etc projects.

Yes, I make "work trees" in a generic sense not just in the `git worktree` 
sense.

> Yes, a user option (inrended for dir-locals) is likely in order, but users
> such as described above would have to set it in _all_ of their
> work directories.

Not if the repository they use for $HOME is different than the one they
use for ~/work, ~/my/hobby/, ...


        Stefan