# HG changeset patch
# User wenzelm
# Date 1616525235 -3600
# Node ID 4840ce456b4fee84dc213db362c280a977b054e9
# Parent  4e12a6caefb3a0580fc3bf99591bda89fd3d1d3f
enforce full build;

diff -r 4e12a6caefb3 -r 4840ce456b4f src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Mar 23 13:27:15 2021 +0100
+++ b/src/Pure/ROOT.ML	Tue Mar 23 19:47:15 2021 +0100
@@ -356,4 +356,3 @@
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML"
-