summaryrefslogtreecommitdiff
path: root/power/Makefile
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-12-13 18:54:17 +0000
committerAlasdair Armstrong2017-12-13 18:54:17 +0000
commit2682a259a2a4a4ee34ddd6be6ea6f5dc3a3a15b7 (patch)
tree8d8ac9d07cc824c2a6c887f345b2865802c4b8ff /power/Makefile
parentb37a6de931c71a3d1136fee74885b5864c24c5c9 (diff)
parent8dde03d441a322fc489e4d25e16cd75d02f64474 (diff)
Merge remote-tracking branch 'origin/master' into interactive
Diffstat (limited to 'power/Makefile')
-rw-r--r--power/Makefile4
1 files changed, 0 insertions, 4 deletions
diff --git a/power/Makefile b/power/Makefile
index 9559646c..f7c49e00 100644
--- a/power/Makefile
+++ b/power/Makefile
@@ -16,10 +16,6 @@ power.ml: power.lem ../src/lem_interp/interp_ast.lem
power_embed.lem: $(SOURCES)
# also generates power_embed_sequential.lem, power_embed_types.lem, power_toFromInterp.lem
$(SAIL) -lem -lem_lib Power_extras_embed -o power $(SOURCES)
- # patch:
- rm -f power_embed.lem power_embed_sequential.lem
- cp power_embed.lem.fixed power_embed.lem
- cp power_embed_sequential.lem.fixed power_embed_sequential.lem
clean:
rm -f power.lem power.ml