[ci docs] Account for gridtk which has a non-standard name (!63) · Merge requests · bob / bob.devtools · GitLab

Snippets Groups Projects

Merged Amir MOHAMMADI requested to merge docs into master 5 years ago

Activity

Amir MOHAMMADI enabled an automatic merge when the pipeline for 6a3c107d succeeds 5 years ago

enabled an automatic merge when the pipeline for 6a3c107d succeeds
Amir MOHAMMADI merged 5 years ago

merged
Amir MOHAMMADI mentioned in commit d763be1b 5 years ago

mentioned in commit d763be1b

Please register or sign in to reply