diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-10-09 23:41:05 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-10-09 23:41:05 -0400 |
| commit | 8a834573a5997e7d069f438470d212bc8fa0a05e (patch) | |
| tree | a803d198a8108f474535997f80cc8e93df1c7768 /src | |
| parent | 32112efcb3522acbece4515b849d40973e48c973 (diff) | |
Restore Redirect in comment blocks
They were there for a reason, which is that the embedded python script
has support for automatically picking up the files in /tmp, so it's nice
to be able to just uncomment the block of code to get the files in /tmp
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v index ab610531f..c991c3454 100644 --- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v +++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v @@ -89,8 +89,8 @@ Module Compilers. (* Set Printing Coercions. - (* Redirect "/tmp/pr" Print Compilers.ident.ident. *) - (* Redirect "/tmp/sm" Show Match Compilers.ident.ident. *) + Redirect "/tmp/pr" Print Compilers.ident.ident. + Redirect "/tmp/sm" Show Match Compilers.ident.ident. *) (* <<< @@ -905,8 +905,8 @@ Module Compilers. (""" + """* Set Printing Coercions. - (* Redirect "/tmp/pr" Print Compilers.ident.ident. *) - (* Redirect "/tmp/sm" Show Match Compilers.ident.ident. *) + Redirect "/tmp/pr" Print Compilers.ident.ident. + Redirect "/tmp/sm" Show Match Compilers.ident.ident. *""" + """) """ |