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

git-push into a repository doesn't start jobs #1779

Open
eugenk opened this issue Aug 12, 2016 · 2 comments · Fixed by #1782
Open

git-push into a repository doesn't start jobs #1779

eugenk opened this issue Aug 12, 2016 · 2 comments · Fixed by #1782

Comments

@eugenk
Copy link
Member

eugenk commented Aug 12, 2016

When I create a repository
And I clone this git repository locally
And I create some commits in my local git repository
And I push these changes
Then parsing jobs should be started

...but they aren't

@eugenk eugenk added this to the improve stability milestone Aug 12, 2016
@eugenk
Copy link
Member Author

eugenk commented Aug 12, 2016

It seems like this is the case for non-empty repositories, too.

@eugenk eugenk changed the title git-push into an empty repository doesn't start jobs git-push into a repository doesn't start jobs Aug 12, 2016
@tillmo
Copy link
Member

tillmo commented Aug 18, 2016

I encountered the same problem again, see https://ontohub.org/esslli-clone. Only after editing one DOL file via the browser, that file has been analysed.

@tillmo tillmo reopened this Aug 18, 2016
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

Successfully merging a pull request may close this issue.

2 participants