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

Removing obsolete options /mimicVerificationOf, /allowGlobals #4062

Merged
merged 11 commits into from
May 23, 2023

Commits on Mar 20, 2023

  1. Configuration menu
    Copy the full SHA
    0d79e26 View commit details
    Browse the repository at this point in the history

Commits on May 22, 2023

  1. Configuration menu
    Copy the full SHA
    5c6bc75 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    a7b1b01 View commit details
    Browse the repository at this point in the history
  3. Removed /mimicVerificationOf, /allowGlobals; internal renaming of Com…

    …pileVerbose to Verbose
    davidcok committed May 22, 2023
    Configuration menu
    Copy the full SHA
    559ee3d View commit details
    Browse the repository at this point in the history
  4. news and options update

    davidcok committed May 22, 2023
    Configuration menu
    Copy the full SHA
    901990e View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    2d8821e View commit details
    Browse the repository at this point in the history
  6. Just building refman on Mac

    davidcok committed May 22, 2023
    Configuration menu
    Copy the full SHA
    c49b45f View commit details
    Browse the repository at this point in the history
  7. Just building refman on Mac

    davidcok committed May 22, 2023
    Configuration menu
    Copy the full SHA
    3c8b4f0 View commit details
    Browse the repository at this point in the history

Commits on May 23, 2023

  1. Configuration menu
    Copy the full SHA
    7c59cc1 View commit details
    Browse the repository at this point in the history
  2. Merge branch 'master' into cok-remove-options

    davidcok committed May 23, 2023
    Configuration menu
    Copy the full SHA
    fad9c37 View commit details
    Browse the repository at this point in the history
  3. Removing extraneous changes

    davidcok committed May 23, 2023
    Configuration menu
    Copy the full SHA
    0af5af8 View commit details
    Browse the repository at this point in the history