You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
8. Use the `git add` command to add the files you have changed to your proposed commit.
76
+
8. Use the `git add X` command to add changes to file `X` to the commit,
77
+
or `git add .` to add all the changed files.
68
78
69
79
9. Run the command:
70
80
```
@@ -76,14 +86,19 @@ How to make changes
76
86
```
77
87
git push
78
88
```
79
-
11. Go to your fork on Github at `https://github.com/USER_NAME/agda-stdlib` and click the green `Compare & pull request` button to open a pull request.
80
89
81
-
12. The standard library maintainers will then be made aware of your requested changes and should be in touch soon.
90
+
11. Go to your fork on Github at `https://github.com/USER_NAME/agda-stdlib`
91
+
and follow the [official Git instructions](https://help.github.com/en/articles/creating-a-pull-request-from-a-fork)
92
+
to open a pull request to the main standard library repository.
93
+
94
+
12. The library maintainers will then be made aware of your requested
95
+
changes and should be in touch soon.
82
96
83
97
Installing `fix-agda-whitespace`
84
98
--------------------------------
85
99
86
-
This tool is kept in the main agda repository. It can be installed by following these instructions:
100
+
This tool is kept in the main agda repository. It can be installed by
0 commit comments