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

improvements made for ProB #159

Open
wants to merge 14 commits into
base: master
Choose a base branch
from
Open

Commits on Jul 11, 2018

  1. Configuration menu
    Copy the full SHA
    6d9e8eb View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    6f012fa View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    d531a10 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    dd66396 View commit details
    Browse the repository at this point in the history
  5. remove prints

    pkoerner committed Jul 11, 2018
    Configuration menu
    Copy the full SHA
    18a079e View commit details
    Browse the repository at this point in the history
  6. use actual copy vector

    pkoerner committed Jul 11, 2018
    Configuration menu
    Copy the full SHA
    e9e1a53 View commit details
    Browse the repository at this point in the history
  7. Configuration menu
    Copy the full SHA
    dea2aae View commit details
    Browse the repository at this point in the history
  8. use correct length

    pkoerner committed Jul 11, 2018
    Configuration menu
    Copy the full SHA
    4d83e05 View commit details
    Browse the repository at this point in the history
  9. expand copy vector correctly

    pkoerner committed Jul 11, 2018
    Configuration menu
    Copy the full SHA
    88390b3 View commit details
    Browse the repository at this point in the history
  10. Configuration menu
    Copy the full SHA
    ce90ea0 View commit details
    Browse the repository at this point in the history
  11. Configuration menu
    Copy the full SHA
    3f04170 View commit details
    Browse the repository at this point in the history
  12. remove old comments

    pkoerner committed Jul 11, 2018
    Configuration menu
    Copy the full SHA
    53ea240 View commit details
    Browse the repository at this point in the history

Commits on Jul 12, 2018

  1. fix warning I introduced

    pkoerner committed Jul 12, 2018
    Configuration menu
    Copy the full SHA
    6501c83 View commit details
    Browse the repository at this point in the history
  2. get rid of more warnings

    pkoerner committed Jul 12, 2018
    Configuration menu
    Copy the full SHA
    d3c5802 View commit details
    Browse the repository at this point in the history