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

docs: reorder & regroup permutation groups chapter #3309

Merged
merged 3 commits into from
Feb 7, 2024

Conversation

fingolfin
Copy link
Member

No description provided.

@fingolfin fingolfin added documentation Improvements or additions to documentation topic: groups labels Feb 2, 2024
Copy link

codecov bot commented Feb 2, 2024

Codecov Report

Merging #3309 (bb46926) into master (a01fe89) will not change coverage.
Report is 1 commits behind head on master.
The diff coverage is n/a.

Additional details and impacted files
@@           Coverage Diff           @@
##           master    #3309   +/-   ##
=======================================
  Coverage   81.71%   81.71%           
=======================================
  Files         556      556           
  Lines       74126    74126           
=======================================
  Hits        60573    60573           
  Misses      13553    13553           

Copy link
Member

@ThomasBreuer ThomasBreuer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fine with me.
Perhaps fix the two typos.

What is the aim of separate @docs groups without introductory text for each of them?

docs/src/Groups/permgroup.md Outdated Show resolved Hide resolved
docs/src/Groups/permgroup.md Outdated Show resolved Hide resolved
@fingolfin fingolfin enabled auto-merge (squash) February 7, 2024 12:30
@fingolfin fingolfin merged commit 968e9e4 into oscar-system:master Feb 7, 2024
20 checks passed
ooinaruhugh pushed a commit to ooinaruhugh/Oscar.jl that referenced this pull request Feb 15, 2024
@fingolfin fingolfin deleted the mh/perm-docs-structure branch May 29, 2024 15:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Improvements or additions to documentation topic: groups
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants