Skip to content

Commit

Permalink
chore(.vscode): make copyright snippet available
Browse files Browse the repository at this point in the history
  • Loading branch information
gebner committed May 19, 2021
1 parent c5bc601 commit 9e84bcf
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions .vscode/copyright.code-snippets
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
{
"Copyright header for mathlib": {
"scope": "lean",
"scope": "lean4",
"prefix": "copyright",
"body": [
"/-",
Expand All @@ -10,4 +10,4 @@
"-/"
]
}
}
}

0 comments on commit 9e84bcf

Please sign in to comment.