mathlib3
document the change in scripts
#1024
Merged

document the change in scripts #1024

PatrickMassot merged 2 commits into master from scripts-docs
cipher1024
cipher1024 document the change in scripts
3beef241
cipher1024 cipher1024 requested a review from PatrickMassot PatrickMassot 7 years ago
cipher1024 cipher1024 requested a review 7 years ago
cipher1024 cipher1024 assigned PatrickMassot PatrickMassot 7 years ago
PatrickMassot Merge branch 'master' into scripts-docs
a3e04e17
PatrickMassot PatrickMassot merged 82f151f5 into master 7 years ago
PatrickMassot PatrickMassot deleted the scripts-docs branch 7 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
Labels
Milestone