Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 81
    • Issues 81
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 10
    • Merge requests 10
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • stdpp
  • Merge requests
  • !371

Clarify relationship between `gset_to_gmap` and `set_to_map`.

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/gset_to_gmap into master Mar 30, 2022
  • Overview 2
  • Commits 1
  • Pipelines 1
  • Changes 1

As a response to a question by @jung at Mattermost: https://mattermost.mpi-sws.org/iris/pl/xdgqgkyw9ifcmj3zdsy8dyb18e I added some comments.

Aside from the differences pointed out in the added comments, the gset function was there before the generic set function.

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: robbert/gset_to_gmap