Code

CL echos the source file name#2675

Code

Merged

tautschnig merged 1 commit intodevelopdiffblue/cbmc:developfrom

goto-cl-echo-filediffblue/cbmc:goto-cl-echo-fileCopy head branch name to clipboard

Aug 6, 2018

Commits

Commits on Aug 4, 2018

• CL prints the name of the file that's compiled onto stdout

  

  Daniel Kroening

  committed
  a66ab1e

  Copy full SHA for a66ab1e