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

checkout bot: use full path for marks files #745

wants to merge 1 commit into from
Changes from all commits
File filter

Filter by extension

Filter by extension

Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
@@ -55,7 +55,7 @@ public List<Bot> create(BotConfiguration configuration) {
var fromBranch = new Branch(from.substring(lastColon + 1));
var to = Path.of(repo.get("to").asString());

var repoName = Path.of(fromURI.getPath()).getFileName().toString();
var repoName = fromURI.getPath();
var markStorage = MarkStorage.create(marksRepo, marksUser, repoName);

bots.add(new CheckoutBot(fromURI, fromBranch, to, storage, markStorage));
@@ -84,7 +84,7 @@ private static Set<Mark> deserialize(String current) {

static StorageBuilder<Mark> create(HostedRepository repo, Author user, String name) {
return new StorageBuilder<Mark>(name + ".marks.txt")
return new StorageBuilder<Mark>(name + "/marks.txt")
.remoteRepository(repo, "master",,, "Updated marks for " + name)
@@ -69,6 +69,8 @@ private static Repository tryMaterialize(HostedRepository repository, Path local
} catch (IOException ignored) {
// The remote ref may not yet exist
Repository localRepository = Repository.init(localStorage, repository.repositoryType());
var file = localStorage.resolve(fileName);
var storage = Files.writeString(localStorage.resolve(fileName), "");
var firstCommit = localRepository.commit(message, authorName, authorEmail);