Code

Fixing order of --warn_error#2952

Code

Merged

mtzguido merged 3 commits intomasterFStarLang/FStar:masterfrom guido_warn_errorFStarLang/FStar:guido_warn_errorCopy head branch name to clipboardJun 6, 2023

+7-4

Commits

Commits on May 31, 2023

• options: fix the order of warn_error

  Show description for 61e742a
  mtzguido

  committed
  61e742a

  Copy full SHA for 61e742a

• snap

  mtzguido

  committed
  d24c8af

  Copy full SHA for d24c8af

Commits on Jun 6, 2023

• Merge branch 'master' into guido_warn_error

  mtzguido

  authored
  bcd8579

  Copy full SHA for bcd8579