# HG changeset patch
# User wenzelm
# Date 1473189453 -7200
# Node ID 3a75593e9b6d1d0c41d1d38d8c02e5a585b6357b
# Parent  67b091896158d297c97fb05996e7e273730f48a3
more operations;

diff -r 67b091896158 -r 3a75593e9b6d src/Pure/General/sqlite.scala
--- a/src/Pure/General/sqlite.scala	Tue Sep 06 21:09:18 2016 +0200
+++ b/src/Pure/General/sqlite.scala	Tue Sep 06 21:17:33 2016 +0200
@@ -29,6 +29,8 @@
 
     def close { connection.close }
 
+    def rebuild { using(statement("VACUUM"))(_.execute()) }
+
     def transaction[A](body: => A): A =
     {
       val auto_commit = connection.getAutoCommit